CNF e Forma Clausal

Uma fórmula na forma normal conjuntiva (abreviado CNF, de Conjuntive Normal Form) é uma fórmula que consiste de uma conjunção de cláusulas.

Uma cláusula é uma fórmula que consiste de uma disjunção de literais.

Um literal é uma fórmula atómica (literal positivo) ou a negação de uma fórmula atómica (literal negativo).

• Nota: na lógica proposicional uma fórmula atómica é uma proposição.

Forma clausal é a representação de uma fórmula CNF através do conjunto das respectivas cláusulas.

Conversão de uma Fórmula Proposicional para CNF e forma clausal

Através dos seguintes passos:

• Remover implicações.

• Reduzir o âmbito de aplicação das negações.

• Associar e distribuir até obter a forma CNF.

Exemplo:

• Fórmula original:

  • A => (B ^ C)

• Após remoção de implicações:

  • ~A V (B ^ C)

Conversão para forma clausal em Lógica de Primeira Ordem - I

Renomear variáveis, de forma a que cada quantificador tenha uma variável diferente.

Remover as implicações.

Reduzir o âmbito das negações, ou seja, aplicar a negação.

Para estas transformações, aplicar as regras de substituição já apresentadas.

Exemplo

Fórmula original:

Variáveis renomeadas:

Implicações removidas:

Negações aplicadas:

II

Skolemização

Nome dado à eliminação dos quantificadores existenciais.

Substituir todas as ocorrências de cada variável quantificada existencialmente por uma função cujos argumentos são as variáveis dos quantificadores universais exteriores.

Remover quantificadores universais.

Exemplo

Skolemizada aplicada:

Quantificadores removidos:

III

Converter para CNF.

• Usar as regras de substituição relativas à comutação, associação e distribuição.

Converter para a forma clausal, ou seja, eliminar conjunções.

Renomear variáveis de forma a que uma variável não apareça em mais do que uma fórmula.

Exemplo

Convertida para a forma clausal:

Variáveis renomeadas:

Lógica - Regras de Inferência

Regras de Inferência específicas

Instanciação universal:

Generalização existencial: