Prova Automática de Teorema

Segundo (), a prova automática de teoremas (Automatic Theorem Proving - ATP) pode ser resumida em: um programa de computador que mostra se uma sentença (a conjectura) é uma conseqüência lógica de um conjunto de sentenças (os axiomas e hipóteses). A linguagem utilizada pelos programas de ATP deve ser formal de modo a não permitir ambigüidade.

A verificação de uma sentença produzida por um programa de ATP é conhecida como prova. Esta prova descreve uma sequência de passos (conseqüências lógicas) que validam uma conjectura. Os passos seguidos por um programa de ATP (conhecidos também como árvore de prova) podem ser compreendidos e seguidos por outros programas de ATP ou mesmo por uma pessoa. Alguns trabalhos pioneiros no desenvolvimento de provadores automáticos de teoremas de Geometria foram (), () e ().

Os programas de ATP, em princípio, devem ser capazes de resolver uma infinidade de problemas, gerando diferentes tipos de provas que dependem dos métodos utilizados (, ,). Atualmente, existem vários métodos para a prova automática em Geometria, dentre eles segundo (, ), merecem destaque: o método de Wu, o método de área, a base de Groebner, o método por vetor e o método por ângulos.

Existem alguns programas de geometria dinâmica (GD) que utilizam os métodos apresentados acima para fazer a prova automática de teoremas. Dentre eles podemos citar os programas Geolog (, ), Geometry Expert (, ) e o Discover (, ).

Na Figura é apresentado a árvore de prova criada pelo programa Geolog (, ) para verificar se é verdadeira a conjectura ``O ponto $E$ é ponto médio de A e B'' a partir da construção realizada.

Figura: Árvore de provaconstruida no programa Geolog

Para (), a Geometria é uma importante área de aplicação da prova automática de teoremas, pois é possível fazer uso de vários métodos para criar provas matemáticas das mais diversas conjecturas geométricas. Contudo, segundo (, ), devido a complexidade do problema (provar), ainda existem algumas limitações nos métodos de ATP que não permitem a prova automática de qualquer figura geométrica.

Neste trabalho, não utilizaremos o método de ATP para validar os exercícios.