Provadores Automáticos de
Teoremas
Estudo e estado da arte dos provadores
automáticos de teoremas
Everton Marques
[email protected]
Agenda





Introdução
Provadores automáticos de teoremas:
fundamentos teóricos
Estado da arte: Provadores automáticos
de teoremas em lógica de primeira
ordem
Estado da arte: Outros tipos de
provadores
Conclusões
Introdução


As pesquisas direcionadas à área de teoria da
prova estudam os conceitos de provas formais e os
fundamentos relacionados
Provas formais podem ser classificadas como:



Prova dirigida por humanos
Prova automatizada
O uso de provadores é bastante difundido na área
de construção de provas formais

Diversas lógicas



Lógica de primeira ordem
Lógica clássica proposicional
...
Introdução

Utilização de diversos métodos






Resolução
Tableaux
Anéis booleanos
Dedução Natural
...
Provador automática de teoremas: um programa
computacional que mostra se a conjectura
apresentada é uma conseqüência lógica de um
conjunto de sentenças (os axiomas e hipóteses)


Linguagem formal sem ambigüidades
Sentença produzida: prova
Provadores automáticos de
teoremas: fundamentos teóricos

Herbrand: desenvolveu a base dos provadores
automáticos de teoremas em 1930.


Seu método era impraticável de se aplicar até a invenção
do computador digital.
Só após o artigo de Robinson em 1965, junto com o
desenvolvimento do princípio da resolução, foi possível o
desenvolvimento dos provadores.
Fundamentos teóricos: Teorema
de Herbrand

Por definição, uma fórmula válida é uma fórmula
que é verdade sobre todas as interpretações.



Herbrand desenvolveu um algoritmo para encontrar uma
interpretação que pode falsificar uma dada fórmula.
Se a dada fórmula mantém-se válida, não pode existir
nenhuma interpretação e seu algoritmo irá parar depois
de um número finito de tentativas.
Desta forma, ao invés de provar se uma fórmula é válida,
o algoritmo de Herbrand prova que a negação da fórmula
é inconsistente
Fundamentos teóricos: Teorema
de Herbrand

Com base no teorema de Herbrand, Gilmore foi um
dos primeiros a implementar o procedimento de
Herbrand em um computador.



Seu programa foi desenvolvido para detectar a
inconsistência da fórmula dada, mas encontrou
dificuldades com fórmulas não simples.
Estudos do seu programa revelaram que o seu método
era ineficiente. O seu método foi melhorado por Davis e
Putnam (1960).
O procedimento de prova por resolução é muito mais
eficiente que os outros métodos anteriores.
Estado da arte: Provadores em
lógica de primeira ordem

CADE – Conference on Automated Deduction




Principal fórum internacional para a apresentação de
pesquisas em todos os aspectos da dedução automática.
1ª vez em 1974. Era bienal até 1996, após anual
Em 2001 uniu-se a outras conferências e virou
International Joint Conference on Automated Reasoning
CASC – CADE ATP System Competition


Foi criada para estimular a pesquisa e desenvolvimento
de sistemas na área dos provadores
Foi criada também para expor sistemas de provas para a
comunidade dos provadores e para fora dela
Estado da arte: Provadores em
lógica de primeira ordem

Avalia o desempenho dos provadores em termos de:



No contexto de:



Número de problemas resolvidos com ou sem solução de sáida
Média de tempo de execução dos problemas resolvidos
Um número limitado de problemas qualificados, escolhidos da
“TPTP Problem Library”
um determinado tempo limite para cada tentativa de solução
A CASC divide-se em classes e na última edição foram 6:






FOF – axiomática FOF com uma conjectura provável
CNF – conjunto de cláusulas insatisfatíveis
FNT – axiomas FOF com conjecturas que não podem ser provadas
SAT – conjunto de cláusulas satisfatíveis
EPR – conjunto de cláusulas finitas
UEQ – cláusulas de unidade equitativas insatisfatíveis
Estado da arte: Vampire

Baseado na CASC é possível falar dos melhores
provadores em lógica de primeira ordem:

Vampire



Desenvolvido na universidade Uppsala pelo PhD Andrei Voronkov e
pelo doutor Alexandre Riazanov
Utiliza métodos de resolução e paramodulação para encontrar bons
resultados de prova
Ganhou muitos prêmios na CASC, e na última competição, a versão
8.1 venceu a divisão CNF e a versão 9.0 venceu a divisão FOF
Estado da arte: Paradox

Paradox






Desenvolvido na Chalmers University of Technology por Koen
Lindström Claessen e Niklas Sörensson
É um provador baseado no método MACE
O método MACE basicamente transforma o conjunto de cláusulas e
um domínio em um conjunto de cláusulas em lógica proposicional
através da introdução de variáveis proposicionais
Venceu a classe SAT do CASC de 2003 até 2006
Em 2007 venceu tanto a classe SAT quanto a FNT
Foi desenvolvido na linguagem Haskell e é um software livre
Estado da arte: Darwin

Darwin





O Darwin é a primeira implementação do cálculo de evolução de
modelos
Possui algumas das técnicas mais eficazes de busca desenvolvidas
pela comunidade SAT
A abordagem é semelhante a outros buscadores de modelos finitos
como o Paradox, mas, em vez de transformar um problema em
lógica proposicional, ele é convertido em lógica de primeira ordem
livre de função.
A versão 1.3 venceu a classe EPR em 2006 e uma variante do
Darwin conseguiu o terceiro lugar na classe SAT
No CASC-21 venceu a classe EPR
Estado da arte: WALDMEISTER

WALDMEISTER





Foi desenvolvido na University of Kaiserslautern por Buch e
Hillenbrand e foi implementado em C
É um provador de teoremas para lógica equacional de primeira
ordem
Tem como objetivo principal ser eficiente em todo o processo de
busca da prova
É dividido em 3 níveis lógicos: nível mais alto corresponde à
escolha dos parâmetros redução ordenada e heurística de busca,
nível intermediário corresponde à uma máquina de inferência e o
nível mais baixo fornece algoritmos e estruturas de dados para a
execução das operações básicas
Vem vencendo a classe UEQ do CASC desde 1997 e a sua última
versão é a WALDMEISTER 806
Estado da arte: E-SETHEO

E-SETHEO







É um provador composicional com estratégia paralela.
Combina uma variedade de provadores de alto desempenho e
procedimentos de decisão especializados
Deixa diferentes procedimentos de busca de provas competirem por
recursos para resolver um determinado problema
Seu sucesso é parcialmente explicado pelo uso de estratégias
paralelas e pela fácil adaptação a um determinado domínio exigido.
Outra importante razão é o uso de excelentes máquinas de
inferência para as diferentes estratégias.
Usa estratégias de cooperação baseadas no lema de intercâmbio
entre os diferentes sistemas
Venceu o CASC-17 nas classes MIX e SEM. Já no CASC-JC
venceu nas classes FOF, MIX e EPR.
Estado da arte: Outros tipos de
provadores

Um Provador Automático de Teoremas para a Lógica
Modal, Baseado em Anéis Booleanos






Desenvolvido no IME-SP por Fabio Campos Tisovec
Tem como objetivo principal ser um provador com um bom grau de
eficiência na prova de problemas SAT
Usa a teoria de anéis booleanos para apoiar a resolução de
problemas de satisfatibilidade
Basicamente pega a expressão trabalhada e subdividi-a em
inúmeras mini-expressões, compara-as duas a duas, e verifica a
existência de contradições entre elas. Caso encontre contradição,
sabe-se que a expressão não é válida, caso contrário ela é aceita
Possui uma estrutura dividida em módulos
A linguagem de programação utilizada foi a C++
Estado da arte: Outros tipos de
provadores

Kems – Um provador de teoremas multi-estratégia





Foi desenvolvido na USP como tese de doutorado de Adolfo Neto.
É um provador multi-estratégia baseado no método de tableaux KE.
É capaz de provar teoremas em três sistemas lógicos: lógica
clássica proposicional, mbC e mCi
Pode ser utilizado com 3 objetivos: educacional, exploratório e
adaptativo
Possui uma arquitetura modularizada
Estado da arte: Outros tipos de
provadores

Dada a entrada, retorna uma prova de saída que contêm:







O status do tableau
A árvore tableau de prova
O tamanho do problema
O tempo gasto para construir a prova
O tamanho da prova
A versão atual é implementada em Java 1.5 e na linguagem
AspectJ
Foi avaliado com várias instâncias de famílias de problemas e
nenhuma configuração do KEMS obteve resultados incorretos.
Estado da arte: Outros tipos de
provadores
Estado da arte: Outros tipos de
provadores

Isabelle








Desenvolvido pela “University of Cambridge” (PhD Larry Paulson) e
“Technical University of Munich” (PhD Tobias Nipkow)
A principal aplicação é a formalização de provas matemáticas e em
particular verificação formal, incluindo provar propriedades de
protocolos e linguagens computacionais
Boa interface visual para o usuário
Ampla documentação, incluindo um tutorial de como usar o sistema
Várias interfaces com outros sistemas
Vem com uma grande biblioteca teórica de matemáticas
Foi utilizado para formalizar muitos teoremas da matemática e da
ciência da computação, como o teorema da completude de Gödel
É um software livre
Estado da arte: Outros tipos de
provadores
Estado da arte: Outros tipos de
provadores

Ergo







Começou o seu desenvolvimento em 2006 na Universidade de Paris
É um provador dedicado a verificação de programas
É baseado no CC(X), um algoritmo de conclusão de congruência e
no cálculo de seqüentes
É implementado em Qu-Prolog
Sua arquitetura é modular
É um software livre
ARA



É um provador para vários tipos de relações algébricas
Pode provar muitos teoremas em diversas álgebras
Foi implementado em Haskell
Estado da arte: Outros tipos de
provadores

PLLIC - Provador para as Lógicas Linear, Intuicionista e
Clássica








Foi desenvolvido no ano de 2006 na universidade UFMG
Foi desenvolvido com a linguagem de programação Java e λ-Prolog
Analisa quando seqüentes do tipo Γ├ L Δ tem resposta: sim ou não,
e caso positivo exibe a prova
Trabalha com 3 tipos de lógica: linear, intuicionista e clássica
É acessado via web e é em português
Possui tutoriais, exemplos e fundamentação teórica também em
português
É fácil de usar e possui uma interface com o usuário agradável
Tem como objetivo principal ser uma ferramenta de fácil manuseio,
podendo ser acessado remotamente para o ensino de lógica em
cursos de graduação
Estado da arte: Outros tipos de
provadores
~((~ A)/\(~B)) |- A\/B
A |- ~(~A) - Dupla negação
Conclusões

Considerações finais




Embasamento teórico
Estado da arte dos provadores
Estudo de muitos provadores
Dificuldades Encontradas



Escolha de escopo
Dificuldade em encontrar bibliografia
Dificuldade na execução dos programas
Conclusões

Trabalhos Futuros



Implementar um provador automático de
teorema
Uma tese de mestrado na área
Desenvolver um provador para competir na
CASC
Referências

MARQUES, Everton. Estudo e estado da arte
dos provadores automáticos de teoremas.
Trabalho de Graduação, Bacharelado em
Ciência da Computação, Universidade Federal
de Pernambuco. 2008.
Provadores Automáticos de
Teoremas
Estudo e estado da arte dos provadores
automáticos de teoremas
Everton Marques
[email protected]