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 frequentemente causam o crescimento [[Função exponencial|exponencial]] no tamanho da fórmula resultante.
O procedimento começa com qualquer fórmula da [[Lógica]] Clássica de Primeira Ordem (LCPO):
Linha 5:
#Coloque a fórmula na Forma Normal Negativa;
#Skolemize - substitua as variáveis existenciais por
#* <math>\exists x. P(x)</math> torna-se '''P(c)''', onde c é novo.
Linha 17:
# 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>.
#* Se m=0 e n=1, isto é um fato do [[Prolog]].
#* Se m>0 e n=1, isto é uma regra do Prolog.
#* Se m>0 e n=0, isto é uma consulta do Prolog.
# Finalmente, substitua cada [[Conjunto|conjunto]] <math>( A1 \wedge ... \wedge Am ) \to ( B1 \vee ... \vee Bn )</math> por <math>\{ A1 \wedge ... \wedge Am \to B1 , A1 \wedge ... \wedge Am \to B2 , ... , A1 \wedge ... \wedge Am \to Bn \}</math>.
Quando n=1, a lógica é chamda de lógica da cláusula de Horn e é equivalente, do ponto de vista
== Veja também ==
| |||