First-Order Logic: normal forms, revisited 1.4 2004/07/01 12:53:20 GMT-5 2004/08/09 16:10:39.813 GMT-5 Ian Barland ian@cs.rice.edu John Greiner greiner@cs.rice.edu Phokion Kolaitis kolaitis@cse.ucsc.edu Moshe Vardi vardi@cs.rice.edu Matthias Felleisen matthias@ccs.neu.edu John Greiner greiner@cs.rice.edu Ian Barland ian@cs.rice.edu Using CNF and DNF with first-order-logic.

CNF and DNF revisited (Optional) In first-order logic, normal forms are still useful for providing a notion of a canonical form. However, their other benefit of corresponding closely to truth tables does not apply here, since truth tables aren't useful for first-order logic. A formula in Prenex Conjunctive Normal Form, or Prenex CNF, has a body in CNF preceded by a series of quantifiers. Similarly, a formula in Prenex Disjunctive Normal Form, or Prenex DNF, has a body in DNF preceded by a series of quantifiers. Assuming φ is in CNF, then the following are each in prenex CNF. On the other hand, if φ is in DNF, these are in prenex DNF. φ ∀x. φ ∃x. ∀y. ∃z. φ Every formula has an equivalent prenex CNF formula and equivalent prenex CNF formula. For brevity, we'll skip proving this.