•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.