ABSTRACT
We will now study normal forms. Generally, by a normal form formula we mean a formula with some limitation on its syntactic form. The reader recalls that we introduced formulas as textual representations of some labeled trees. One, then, can think about formulas as trees. This was very useful, because trees have rank function, and so various arguments were easier. We can also think about formulas as representations of tables. Many formulas may (and in fact will) represent a single table, and we may want to use some specific representations. These representations are limited by the syntactic form we allow. It turns out that it makes a lot of difference how we represent formulas. If we think about formulas as representing constraints on valuations (namely that a valuation needs to satisfy the formula) then the specific syntactic form we use to represent constraints may make a lot of difference. In fact, having a specific syntactic form of a formula may make the task of testing some properties entirely trivial. For instance, if we have a formula ϕ in disjunctive normal form then testing its satisfiability is very easy. Likewise, testing a conjunctive normal form for being a tautology is completely trivial. The only problem with this approach is that finding the disjunctive (resp. conjunctive) normal form of a formula is an expensive task in itself. But there are often advantages. For instance, if we have a formula ϕ in conjunctive normal form and we are testing satisfiability, then there is an additional mechanism (called Boolean constraint propagation) that can be used to speed up the DPLL process by cutting portions of the search tree. Moreover, in the same case of conjunctive normal form, we have a general processing technique, called resolution, that can be used to test satisfiability. First, we will discuss a simpler normal form, called negation normal form. This normal form preserves polarity and will be useful when we discuss the Craig lemma. We will also discuss “complete forms” of disjunctive and conjunctive normal forms, and connection between conjunctive and disjunctive normal forms. This allows us to get a better handle on the Lindenbaum algebra of the language. The completeness results for sets of functors always produce normal form (in fact
gives some In this will discuss implicational normal form, this one involving the fact that the functor ⇒ forms by itself a complete set of functors (in a weak sense, that is in the presence of constants) and the ite-normal form, again the consequence of the fact that ite is (weakly) complete. Finally, we notice that there exist normal forms involving NAND and NOR. These are of practical importance, but we will not discuss them here.
