Lógicas Clássicas
Prova Automática de Teoremas
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.