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.

Answer 2

Steps that can be followed for CNF Conversion First-Order Logic 
Removal of Implications 
Replace Implications with its logical equalities. 
 
Thus,. 
P→Q becomes  
eg P¬Q 
eg P ∨ Q. 
 
Moving Negation In 
Use DeMorgan Law and Quantifiers to move a negation from the conjunction or disjunction of quantified statements of variables 
Use the rules 
¬(P,Q)¬∃x((P(x)):¬P ¬Q =¬P ∪¬Q¬(P⋁Q) ¬∀x(P)¬∀x(Q)¬Q¬PQ¬∃xPx¬∀x Q¬∂xQ(X)¬P¬ Q¬∃x(R)¬(∃xQ(Q)) (¬P),¬((Q)) ). 
 
Skolemization: Replace existential quantifiers by Skolem functions or constants to eliminate them. 
 
c whenever there are no universal quantifiers in scope. In case there are some, then replace ? by the Skolem function ? 
 
Drop Universal Quantifiers: Once you have done Skolemization, you can remove the universal quantifiers, as any remaining variables are implicitly universally quantified. 
 
Distribute OR over AND: Distribute disjunctions (ORs) over conjunctions (ANDs) to get the expression into CNF. 
 
For example, convert 
P ∨(Q∧R) 
P∨(Q∧R) to(P∨Q)∧(P∨R) 
(P∨Q)∧(P∨R). 
Final Form: The final result will be a conjunction of disjunctions, which is the CNF form.