Um estudo do sistema Oyster-Clam, implementação de reescrita de tipos e uma formalização parcial da teoria dos grafos

AUTOR(ES)

Jeronimo Pellegrini

DATA DE PUBLICAÇÃO

1997

RESUMO

Nesta tese, mostramos uma implementação do processo de diagonalização de Cantor no sistema de prova de teoremas Oyster-Clam. Para isto, tivemos que estender o Oyster com comparação e indução em tipos, e desenvolvemos um método e algumas regras de reescrita. As regras de reescrita lidam com tipos, o que não era suportado ainda no sistema Oyster-Clam; algumas modificações foram feitas para que isto se tornasse possível. Também desenvolvemos esquemas de indução para grafos neste sistema, e provamos alguns teoremas

ASSUNTO(S)

demonstração automatica de teoremas inteligencia artificial logica simbolica e matematica

Documentos Relacionados

• Uma formalização da teoria de reescrita em linguagem de ordem superior
• DefiniÃao e implementacÃo do sistema de tipos da linguagem Circus
• Uma introdução à teoria dos grafos no ensino médio
• Algoritmos para emparelhamento em grafos e uma implementação paralela
• Projeto e estudo de caso da implementação de um sistema de controle nebuloso