Método das Bases de Dados Deductivas para a Geometria (Dedução Automática na Geometria)

Abstract

Os provadores automáticos de geometria são programas que permitem desenvolver demonstrações formais para conjecturas geométricas de forma automática sem intervenção humana. Têm como objetivo principal a decisão, em tempo útil e relativamente a um conjunto de condições iniciais, do valor lógico de uma conclusão estabelecida. Originalmente concebidos durante a década de 50, permitem o desenvolvimento de demonstrações formais, em alguns casos produzindo uma versão legível por um matemático. Este relatório tem como objetivo providenciar uma introdução ao conceito de provadores automáticos de geometria, uma introdução básica dos principais métodos e com um interesse principal no método das bases de dados dedutivas. Introduz a história dos provadores automáticos, as diferentes áreas que auxiliaram o desenvolvimento e alguns dos diferentes sistemas utilizados atualmente. A secção conclui com uma breve introdução aos diferentes métodos disponíveis e uma primeira visão do método das bases de dados dedutivas. Finalmente, é introduzido um programa, criado com a esperança de resolver problemas geométricos, utilizando uma lista de regras definida com base em um artigo publicado anteriormente. Devido à complexidade do projecto e ao tempo limitado para o executar, o programa desenvolvido, emboracompleto, ainda necessita de algum trabalho para efeitos de eficiência, tanto em termos de tempo,como taxa de sucesso. São documentadas as dificuldades ultrapassadas durante o seu desenvolvimento, os limites presentes no sistema e conjunto de regras utilizadas como base para o programa, bem como os problemas identificados durante o desenvolvimento do programa.

Automatic geometry provers are programs that allow you to develop formal proofs for geometric conjectures automatically without human intervention. Their main objective is to decide, in good time, and in relation to a set of initial conditions, the logical value of an established conclusion. Originally conceived during the 1950s, they allow the development of formal proofs, in some cases producing a version readable by a mathematician. This report aims to provide an introduction to the concept of automatic geometry provers, a basic introduction to the main methods and with a main interest in the method of deductive databases. It introduces the history of automated theorem provers, the different areas that helped their development and some of the different systems used today. The section concludes with a brief introduction to the different methods available and a first view of the method of deductive databases. Finally, the implementation of the deductive database method is described. Created with the hope of solving geometric problems, using a list of rules defined based on an article previously published. Due to the complexity of the project and the limited time to execute it, the developed program, although complete, still needs some work for efficiency purposes, both in terms of time and success rate. The difficulties overcome during its development, the limits present in the system and set of rules used as a basis for the program, as well as the problems identified during the development of the program are documented.