PROVADORES DE TEOREMAS:
Visão Geral
André Luiz de Lacerda
Ricardo Trizzolini Piekarski
1
Introdução - Objetivo
• O que são provadores de teoremas?
• Exemplos
• Aplicações
• Peculiaridades
2
"Fonte: SXC. Xadrez. Disponível em: <http://www.sxc.hu/browse.phtml?f=view&id=739384>. Acesso em: 7 maio 2009."
Introdução - Conceito
• Ferramentas
• Programas de computador
• Conjunto de sentenças → Consequência lógica
• Não restrito às exatas
• Automated Theorem Provers (ou ATPs)
• CASC
3
Tipos de provadores
Baseados em métodos
• Resolução
• Tableaux Analíticos
• Tableaux KE
4
"Fonte: SXC. Tarefa de Lógica. Disponível em: <http://www.sxc.hu/browse.phtml?f=view&id=860172>. Acesso em: 7 maio 2009."
Baseados no método da Resolução
EQP (Equational Theorem Prover)
Lógica equacionais de primeira ordem
↑ Boas implementações de unificação
↑ Correspondência associativo-comutativa
↑ Estratégias para raciocínio equacional
↑ Buscas rápidas
5
Baseados no método da Resolução
EQP (Equational Theorem Prover)
↓ Estabilidade
↓ Aparência
↓ Sem garantias
↓ Execução por linhas de comando
6
"Fonte: SXC. Labirinto. Disponível em: <http://www.sxc.hu/browse.phtml?f=view&id=1008265>. Acesso em: 7 maio 2009."
Baseados no método da Resolução
Otter / Mace2
Organized Techniques for Theorem-proving and Effective Research
• Lógicas equacionais de primeira ordem
• Otter → provador de teoremas
• Mace2 → buscador de modelos finitos e
contra-exemplos
7
Baseados no método da Resolução
Otter / Mace2
Organized Techniques for Theorem-proving and Effective Research
↑ 1° de sua categoria a ser amplamente distribuído
↑ Pioneiro em diversas técnicas de implantação
↑ Domínio público
↓ Execução por linhas de comando
↓ Não tem mais sido desenvolvido
8
Baseados no método da Resolução
Prover9 / Mace4
Sucessor do Otter
↑ Constante desenvolvimento
↑ Interface Gráfica
9
"Fonte: Prover9-Mace4 v05. Disponível em: <http://www.cs.unm.edu/~mccune/prover9/gui/v05.html>. Acesso em: 5 maio 2009."
Baseados em Tableaux Analíticos
jTAP – A Tableau Prover in Java
Lógicas equacionais de primeira ordem
↑ Pode ser adaptável a outras lógicas
↑ Implementado em Java
↑ Roda em forma de Applet direto do website
10
Baseados em Tableaux Analíticos
WDTP – Wagner Dias Tableau Prover
•
Estrutura orientada a objetos (Object-oriented
framework) implementada em C++
•
Batizado por Adolfo Neto
•
Adolfo também fez algumas modificações:
–
–
Provas mais curtas em Tableaux KE
Adaptações para Windows XP e Linux
11
Baseados em Tableaux Analíticos
WDTP – Wagner Dias Tableau Prover
↑ Base para implementação de métodos:
‒ Tableaux Analíticos de Smullyan
‒ Tableaux KE de Mondadori e D'Agostino's
‒ Tableaux KE-S3 de Finger e Wasserman
↑ Adaptado ao Windows e Linux
↑ Permite imprimir a árvore de prova completa
↓ Execução em linhas de comando
12
Baseados em Tableaux KE
KEMS (KE-based Multi-Strategy theorem prover)
• Implementado em Java e AspectJ
↑ Multi-estratégia
↑ Interface gráfica
13
"Fonte: SXC. Jogo de Damas. Disponível em: <http://www.sxc.hu/browse.phtml?f=view&id=919928>. Acesso em: 7 maio 2009."
Outros
• Tarski’s World
• Vampire
• PLLIC
• Isabelle
"Fonte: Usando Tarski’s World. Disponível em: <http://www.mat.uc.pt/~picado/ediscretas/apontamentos/Tarski.pdf >. Acesso em: 6 maio 2009. 8 p"
"Fonte: MARQUES, Everton G. Estudo e estado da arte dos provadores automáticos de teoremas: Trabalho de graduação. Disponível em:
<http://www.cin.ufpe.br/~tg/2007-2/egm2.pdf>. Acesso em: 5 maio 2009. Recife, 2008. 65 p"
14
Expectativas
• Cooperatividade
• Um ATP seguindo
padrão internacional
• Divisão de tarefas
• Implementação de
lógicas mais complexas
"Fonte: SXC. Quebra-cabeças. Disponível em: <http://www.sxc.hu/browse.phtml?f=view&id=796887>. Acesso em: 7 maio 2009."
15