您在這裡

CNF and DNF revisited (Optional)

16 六月, 2015 - 15:53
Available under Creative Commons-ShareAlike 4.0 International License. Download for free at http://cnx.org/contents/383d4b87-2d7b-454e-99fe-2eaa43eae8ff@20.20

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 PrenexCNF, has a body in CNF preceded by a series of quantifiers. Similarly, a formula in PrenexDisjunctiveNormalForm, or Prenex DNF, has a body in DNF preceded by a series of quantifiers.

Example 4.10

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.