Normal form

Logical Paradigms in Computing Normal Forms (Continue…) Conjunctive normal forms and validity An algorithm which always computes the same output CNF for a given input φ. This algorithm, called CNF, should satisfy the following requirements: 1. CNF terminates for all formulas of propositional logic as input. 2. For each such input, CNF outputs an equivalent formula. 3. All output computed by CNF is in CNF. If a call of CNF with a formula φ of propositional logic as input terminates, which is enforced by (1), then (2) ensures that ψ ≡ φ holds for the output ψ. Thus,(3)guarantees that ψ is an equivalent CNF of φ. So φ is valid iff ψ is valid. If formula φ is an input then first we have to translate all implications in φ by replacing all sub formulas of the form ψ → η by ¬ψ ∨ η. This is done by a procedure called IMPL FREE. The application of IMPL FREE might introduce double negations into the output formula. If we want to compute a CNF for ¬φ from a CNF for φ then just translate ¬φ as an equivalent formula that contains only negations of atoms. Formulas which only negate atoms are said to be in negation normal form (NNF). Examples of negation normal form (NNF) are given below: The second step is to call NNF with the implication-free output of IMPL FREE to obtain an equivalent formula in NNF. After all this preprocessing, we obtain a formula φ’ which is the result of the call NNF (IMPL FREE (φ)). Note that φ ≡ φ’. It is possible to program CNF by an analysis of only three cases: literals, conjunctions and disjunctions. • If φ is a literal, it is by definition in CNF and so CNF outputs φ. • If φ equals φ1 ∧ φ2, we call CNF recursively on each φi to get the respective output ηi and return the CNF η1 ∧ η2 as output for input φ. • If φ equals φ1 ∨ φ2,we again call CNF recursively on each φi to get the respective output ηi; but this time we must not simply return η1 ∨ η2 since that formula is certainly not in CNF, unless η1 and η2 happen to be literals. Distributivity laws enable us to translate any disjunction of conjunctions into a conjunction of disjunctions which could be applied by using an independent algorithm called DISTR. Pseudo code for CNF is given below: Pseudo code for DISTR is given below: The pseudo code for NNF is given below: Example: Compute CNF (NNF (IMPL FREE (¬p ∧ q → p ∧ (r → q)))). First, compute IMPL FREE (φ): Second, compute NNF (IMPL FREE φ): Third, Compute CNF: Horn clauses and satisfiability: It is difficult to test the satisfiability of the above derived CNF form. An efficient way to do this is to use sub classes of formula. Such an important class is called Horn Class or Horm Formula. A Horn formula is a formula φ of propositional logic if it can be generated as an instance of H in this grammar: ⊥(‘bottom’) denotes an unsatisfiable formula and T(‘top’) denotes a tautology. Horn formulas are conjunctions of Horn clauses. Each instance of C is a Horn clause. A Horn clause is an implication whose assumption A is a conjunction of propositions of type P and whose conclusion is also of type P. For example: The steps to test the satisfiability of a Horn formula φ are given below: 1. It marks T if it occurs in that list. 2. If there is a conjunct P1 ∧ P2 ∧ ···∧ Pki → Pof φ such that all Pj with 1 ≤ j ≤ ki are marked, mark P as well and go to 2. Otherwise (= there is no conjunct P1 ∧ P2 ∧ ···∧ Pki → Psuch that all Pj are marked) go to 3. 3. If ⊥ is marked, print out ‘The Horn formula φ is unsatisfiable.’ and stop. Otherwise, go to 4. 4. Print out ‘The Horn formula φ is satisfiable.’ and stop. Exercise 1. Write a recursive function IMPL FREE which requires a propositional formula as input and produces an equivalent implication-free formula as output. How many clauses does your case statement need? 2. Compute CNF (NNF (IMPL FREE ¬(p → (¬(q ∧ (¬p → q)))))). 3. Computer CNF (NNF (IMPL FREE r → (s → (t ∧ s → r)))). 4. Apply algorithm HORN to each of these Horn formulas: (a)- (p ∧ q ∧ w →⊥) ∧ (t →⊥) ∧ (r → p) ∧ ( T→ r) ∧ (T → q) ∧ (u → s) ∧ ( T→ u) (b)- (T→ q) ∧ (T→ s) ∧ (w →⊥) ∧ (p ∧ q ∧ s → v) ∧ (v → s) ∧ (T→r) ∧ (r → p)