Converting First order logic to CNF

Question

Is there an existing implementation in C/c++/java to convert first-order logic to CNF?

Answer 1

1. Eliminate biconditionals and implications:

• Eliminate ⇔, the replacing α ⇔ β with (α ⇒ β) ∧ (β ⇒ α).

• Eliminate ⇒, then replacing α ⇒ β with ¬α ∨ β.

2. Move ¬ inwards:

• ¬(∀ x p) ≡ ∃ x ¬p,

• ¬(∃ x p) ≡ ∀ x ¬p,

• ¬(α ∨ β) ≡ ¬α ∧ ¬β,

• ¬(α ∧ β) ≡ ¬α ∨ ¬β,

• ¬¬α ≡ α.

3. Regulate the variables apart by renaming them: each quantifier should use a different variable.

4. Skolemize: In this, each existential variable is replaced by a Skolem constant or Skolem function of the

enclosing universally quantified variables.

• For example, this ∃x Rich(x) will become Rich(G1) where G1 is a new Skolem constant.

• “Everyone has a heart” ∀ x Person(x) ⇒ ∃ y Heart(y) ∧ Has(x, y) becomes ∀ x Person(x) ⇒ Heart(H(x)) ∧ Has(x, H(x)),

where H is a new symbol in the given equation (Skolem function).

5. Drop universal quantifiers

• For instance, ∀ x Person(x) becomes Person(x).

6. Distribute ∧ over ∨:

•Now (α ∧ β) ∨ γ  is equivalent to(α ∨ γ) ∧ (β ∨ γ)

For more information regarding the same, refer to the following link: https://en.wikipedia.org/wiki/Conjunctive_normal_form

If you wish to learn about Artificial Intelligence then visit this Artificial Intelligence Course.