Algumas Idéias e Experimentos sobre Demonstração Automática de Teoremas

Este trabalho contém algumas idéias e experimentos sobre Demonstração Automática de Teoremas.

São descritas as pesquisas que o autor realizou durante os últimos cinco anos, dando continuidade ao trabalho de doutorado de Roberto Lins de Carvalho.

Neste trabalho introduziu-se uma estratégia completa para Teorias Definicionais, TRADUÇÃO POR NÍVEL, com ou sem axiomas próprios. Além de analisar-se a consistência das definições por intermédio da construção automática de ESTRUTURAS DEFINICIONAIS.

Além disso os experimentos realizados mostraram, em resumo, que:

(i) as limitações de tempo e memória nos obrigam a sempre organizarmos um provador interativo homem/máquina.

(ii) devemos mudar a estratégia de provas de acordo com a teoria em que estamos trabalhando. Pelo fato de ser um sistema em módulos independentes, isso é possível.

Baseados em (i) e (ii), elaboramos algumas idéias para a criação de um sistema, gerador de provador de teoremas, completamente modular c que ensina ao usuário modificá-lo, isto é, de acordo com resultados parciais de provas naquela teoria, o usuário pode mudar o provador dinamicamente.

Basicamente este sistema consta de dois programas modulares. O primeiro programa com que o usuária tem contato, programa gerador, proporciona a geração de um segundo programa, programa gerado, que será o provador de teoremas da teoria definida pelo usuário, quando da interação com o programa gerador.

As idéias novas introduzidas no trabalho são: gerador de estruturas definicionais, tradução por nível como uma estratégia completa para teorias definicionais e fundamentalmente o fato de podermos gerar um provador mutável com a teoria e ou com o resultado da primeira utilização do provador.