Lógicas Clássicas
Prova Automática de Teoremas
- A TEORIA DA RESOLUÇÃO, proposta por Robinson em 1965 a partir dos trabalhos de Herbrand, Davis e Putnam, parte da transformação da fórmula a ser provada para a forma canônica conhecida como forma clausal.
- O método é baseado em uma regra de inferência única, chamada REGRA DA RESOLUÇÃO, e utiliza intensivamente um algoritmo de casamento de casamento de padrões chamado ALGORITMO DE UNIFICAÇÃO.
- O fato de ser possível associar uma semântica operacional a um procedimento de prova automática de teoremas permitiu a definição de uma linguagem de programação baseada em lógica, a linguagem PROLOG.
- Ainda hoje a área de prova automática de teoremas permanece bastante ativa, sendo objeto de diversas conferências internacionais.