Working Environment for Automated Deduction in Geometry

Abstract

Dadas as suas propriedades formais, lógicas e espaciais, a geometria é adequada para ambientes de ensino que incluam sistemas de geometria dinâmica (DGS), demonstradores automáticos de teoremas para a geometria (GATP) e repositórios de problemas geométricos. Com a ajuda dos DGS, os alunos podem efectuar construções geométricas e conjecturar sobre as propriedades das mesmas. Com os GATP, podem verificar a correcção das construções (por exemplo, se duas linhas dadas são paralelas) e também demonstrar as conjecturas geométricas. Estas ferramentas, apoiadas em repositórios de conhecimento geométrico, fornecem aos professores e alunos um ambiente de trabalho suportado por um conjunto alargado de exemplos de construções geométricas e conjecturas, para o desenvolvimento de experiências.Tem-se como objetivo final contribuir para o desenvolvimento de um ambiente de trabalho, onde as componentes de geometria dinâmica e de dedução automática trabalham em conjunto, providenciando demonstrações em geometria euclidiana, escritas em linguagem natural e com uma apresentação visualmente dinâmica. Citando Gila Hanna “a melhor prova é aquela que também ajuda a entender o significado do teorema a ser demonstrado: perceber que não é apenas verdadeiro, mas também por que é verdadeiro”.Tendo como ponto de partida o trabalho já desenvolvido no projecto de código aberto Open Geometry Prover (OGP), o objetivo inicial era completar o GATP do método de ângulo completo, melhorando a «biblioteca» do OGP, e permitindo à comunidade da dedução automática emgeometria usufruir de uma nova ferramenta. O projecto OGP foi inicialmente desenvolvido pelo aluno de doutoramento Ivan Petrović, sob a orientação de Predrag Janičić da Universidade de Belgrado, Sérvia, não tendo sido, contudo, terminado. Tendo assumido o projeto, agoradesignado como Open Geometry Prover Community Project (OGPCP), optou-se por uma implementação totalmente nova de um GATP baseado no método das bases de dados dedutivas para a geometria, tendo concluído uma primeira versão do demonstrador automático de teoremas,o Geometry Deductive Database Prover, totalmente integrado ao OGPCP.

Given its formal, logical and spatial properties, geometry is well suited to be used in teaching environments that include dynamic geometry systems (DGS), geometry automated theorem provers (GATP) and repositories of geometric problems. With the help of the DGS, students can build geometric constructions and conjecture about their properties. With the GATP, students may check the soundness of the constructions (e.g., if two given lines are parallel) and also create formal proofs of conjectures. These tools, backed by repositories of geometric knowledge, provide teachers and students with a framework supported by a large set of geometric constructions and conjectures, for the development of experiments.The ultimate goal is to contribute towards the development of a working environment, where the dynamic geometry component and the automated deduction component work together, providing proofs for plane geometry, in natural language and with a visually dynamic presentation. Quoting Gila Hanna “the best proof is one that also helps understand the meaning of the theorem being proved: to see not only that it is true, but also why it is true”.Building on the work already done in the open source project Open Geometry Prover (OGP), the initial goal was to complete the GATP based on the full-angle method, improving OGP’s library, and allowing the automated deduction in geometry community to profit from a new tool.The OGP project was originally developed by PhD student Ivan Petrović, under the guidance of Predrag Janičić of the University of Belgrade, Serbia, but it was not completed. Having taken over the project, now designated as the Open Geometry Prover Community Project (OGPCP), it was opted for a totally new implementation of a GATP based on the deductive databases for geometry method, having concluded a first version of the automatic theorem prover, the Geometry Deductive Database Prover, fully integrated in the OGPCP.