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...

Comments
Post a Comment