Forma normal clausal: diferenças entre revisões
Conteúdo apagado Conteúdo adicionado
Linha 1:
A Forma Normal Clausal é usada em [[Programação lógica|programação lógica]] e em muitos sistemas provadores de teoremas. O procedimento de conversão de uma fórmula para a forma clausal pode destruir a estrutura da fórmula e, além disso, traduções feitas de forma indevida
O procedimento começa com qualquer fórmula da [[Lógica
#Coloque a fórmula na Forma Normal Negativa;
#[[Skolemização|Skolemize]] - substitua as variáveis existenciais por constantes de Skolem ou funções de Skolem de variáveis universais, de fora para dentro. Faça as seguintes substituições:
#* <math>\exists x. P(x)</math> torna-se '''P(c)''', onde c é novo.
Linha 13:
#Remova os quantificadores universais
#Coloque a fórmula na [[Formal normal conjuntiva|Forma Normal Conjuntiva]].
# Substitua <math>C1 \wedge ... \wedge Cn</math> por <math>\{C1 , ... , Cn\}</math>. Cada conjunto é da forma <math>\neg A1 \vee ... \vee \neg Am \vee B1 \vee ... \vee Bn</math>, que é equivalente à <math>( A1 \wedge ... \wedge Am ) \to ( B1 \vee ... \vee Bn )</math>.
| |||