Please use this identifier to cite or link to this item: https://hdl.handle.net/10316/114718
Title: Working Environment for Automated Deduction in Geometry
Other Titles: Ambiente de Trabalho para a Demonstração Automática de Teoremas em Geometria
Authors: Baeta, Nuno Miguel dos Santos
Orientador: Almeida, Pedro Henrique e Figueiredo Quaresma de
Keywords: Demonstração Automática; Geometria; Ambiente de Trabalhio; Automatic Deduction; Geometry; Working Environment; -; -; -; -
Issue Date: 21-Feb-2024
Serial title, monograph or event: Working Environment for Automated Deduction in Geometry
Place of publication or event: Departamento de Matemática da Faculdade de Ciências e Tecnologia da Universidade de Coimbra
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.
Description: Tese de Doutoramento em Álgebra Computacional apresentada à Faculdade de Ciências e Tecnologia
URI: https://hdl.handle.net/10316/114718
Rights: openAccess
Appears in Collections:UC - Teses de Doutoramento

Files in This Item:
File SizeFormat
thesis.pdf2.27 MBAdobe PDFView/Open
Show full item record

Page view(s)

11
checked on May 15, 2024

Google ScholarTM

Check


This item is licensed under a Creative Commons License Creative Commons