•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.
•Algumas Definições
–PROVA:
É a demonstração de que um teorema (ou fórmula) é verdadeiro.
–FORMA
NORMAL CONJUNTIVA: É quando uma fórmula F for composta de uma conjunção de outras fórmulas (F1 ^ F2 ^ ... ^
Fn).
–FORMA
NORMAL DISJUNTIVA: É quando uma fórmula F for composta de uma disjunção de outras fórmulas (F1 v F2 v ... v
Fn).
–FORMA
NORMAL PRENEX: É quando numa fórmula F, na lógica de primeira ordem, todos os quantificadores existentes
prefixam a fórmula, isto é,
se e somente se estiver na forma Q1x1...Qnxn(M).
–Onde:
– Qixi = "xi ou $xi, e (M) = uma
fórmula que não
contenha quantificadores.