Logic for Computer Scientists/Propositional Logic/Equivalence and Normal Forms

Equivalence and Normal FormsEdit

Until now, we only discussed single formulae and their semantical properties. In this section we start investigating whether formulae can be transformed into another form, without changing their semantics. For this we introduce the concept of logical equivalence, which can be used to investigate the transformation of a given formula into its normal form.

Definition 6Edit

The formulae   and   are called (semantically) equivalent, iff for all assignments   for   and  ,  . We write  .

Formulae containing different subformulae can be equivalent, e.g. all tautologies are equivalent. More interesting is the following theorem:

Theorem 3 (Substituitivity)Edit

Let   and   a formula which contains at least one occurrence of the subformula  . Then it holds  , where   is obtained from   by substituting any occurrence of   by  .

Proof: The proof is by induction over the structure of the subformula  :

Assume for the induction start, that   is atomic, hence   holds, and the result of substituting the only occurrence of   by   results in   and because  , we have  . Assume the theorem holds for all proper subformulae of  : If   we have the same argumentation as above in the start of the induction. If   we have three cases:

  •  : Because   is a subformula of   we can conclude that  , where   is constructed by substituting any occurrence of   by  . From the definition of the semantics of   we conclude that   and hence  . Where H_1 is equivalent formula constructed by replacing F in H by G, resulting in H_1
  •  : Assume without loss of generality, that   occurs in  . Then, again we can conclude from the induction assumption, that   and from the definition of the semantics of   we conclude, that  .
  •   is similar.

Theorem 4Edit

The following equivalences hold:

     

      (Idempotence)

     

      (Commutativity)

     

      (Associativity)

     

      (Absorption)

     

      (Distributivity)

      (Double negation)

     

      (deMorgan's rule)

     , if   is a tautology

     , if   is a tautology (Rule of Tautology)

     , if   is unsatisfiable

     , if   is unsatisfiable (Rule of Unsatisfiability)


Proof: All equivalences can be proved by truth tables. This is done here for the second rule of absorption:

    ( ) ( ))
false false
false
false
false true
false
false
true false
false
true
true true
true
true

Let us now use these equivalences together with the theorem of substituitivity (TS) to prove the following equivalence:

 



 


    Associativity and TS

    Commutativity and TS

    Distributivity

    Commutativity and TS

    Distributivity and TS

    Unsatisfiability and TS

    Commutativity and TS

    Commutativity and TS


ProblemsEdit

Problem 9 (Propositional)Edit

The binary junctor   for exclusive disjunction is defined by  . Show that the following holds for propositional logic formulae  ,   and  :

  1.   (Commutativity).

  2.   (Associativity)


 

Problem 10 (Propositional)Edit

Show the following by equivalence transformation. Give to all remodelling steps the used rules!

  1.  
  2.  
  3.  
  4.  
  5.  
  6.  


 

Problem 11 (Propositional)Edit

Prove with equivalences:

  1.   is a tautology.
  2.   is unsatisfiable.


 

Problem 12 (Propositional)Edit

The binary junctor   with the meaning neither-nor is defined by  . Let   be a propositional logic formula, which contains only the operators     and  . Prove that for every formula   a formula   exists, such that   and   is built by using only the junctor  .


 

Problem 13 (Propositional)Edit

Let   be a propositional logic formula, which contains only the operators  ,   and  . Prove that for every formula   a formula   exists, such that   and   is built by using only the junctors   and  .

 

Problem 14 (Propositional)Edit

The following formulae are given:

  •  
  •  
  •  



  1. Simplify   by using  .
  2. Simplify   by using equivalences but not  .


 

Definition 7 (Normal Forms)Edit

A literal is an atomic formula or the negation of an atomic formula (positive or negative, resp.) A formula   is in conjunctive normalform (CNF) iff


 

where   is a literal.


A formula   is in disjunctive normalform (DNF) iff

 

where   is a literal

Theorem 5Edit

For every formula   there is an equivalent formula which is in DNF and an equivalent formula which is in CNF.

Let us formulate an algorithm to transform a given formula F into an equivalent normalform:

Given: A formula  


1. Substitute in   every subformula of the form

 
 
 

until there is no subformula of this kind.

2. Substitute in the result from the above step every subformula of the form

 
 

until there is no subformula of this kind.

Result: An equivalent formula in CNF

Until now, we investigate the transformation of a propositional formula into an equivalent normal form. Another problem in the context of normal forms is, to construct a normal form formula from a given truth table; i.e. the formula itself is not known, but its behaviour is given by a truth table. Let's read a normalform formula from a truth table: Assume a formula  , which is given by the following truthtable.


A B C F
false false false true
false false true false
false true false false
false true true false
true false false true
true false true true
true true false false
true true true false

In order to construct a formula in DNF, which is equivalent to  , we have to take into account, that every line of the table which yields the truthvalue   gives one conjunction: if the assignment of the literal   is   it is included as  , if is   we include  . For the above example we get as a DNF:

 

 

 


If we change in the above procedure the roles of   and   and   and   we arrive at a CNF:

 

 

 

 

 


We introduce a special representation for formulae in normalform. In our circuit-example (circuit) from the introduction we already used a very special form of normalforms, namely the implication form for formulae in CNF: every subformula   of a conjunction   is written as:

 

It is easy to see, that this implication is logically equivalent to a disjunction  . Sometimes the implication is written as

 

Even the following ambiguous notation is used in some cases, where the comma in the premiss stands for a conjunction and the comma in the conclusion for a disjunction:

 

For some important procedures for logical reasoning it is mandatory to represent the formulae not only in one of the above notations for a normalform, moreover, it is necessary to use the so-called clause-form from the following definition.


Definition 8Edit

If   is a formula in CNF, i.e.

 

then its corresponding representation in clause form is given as

 

The sets   are called clauses.

This representation as sets of literals has the advantage that literals occur in no special order and that multiple occurrences of a literal in a disjunction are "merged" in its clause form. Note that as a consequence we have built in associativity, commutativity and Idempotence into the representation.

               


 

ProblemsEdit

Problem 15 (Propositional)Edit

Create formulae in (a) conjunctive or (b) disjuncive normal form which are equivalent to:

 


where   denotes exclusive or.


 

Problem 16 (Propositional)Edit

The theorem prover OTTER uses the following optimization rules for clause sets:

Subsumption: If the literals of a clause   are a subset of an another clause   remove   from the set of clauses.
Deleting by unit clause: If the set of clauses contains a unit clause   -here   is single literal unit-clause- every occurrence of a complementary literal   in a clause is deleted.

Which laws of the logic justify these procedures?

 

Problem 17 (Propositional)Edit

Generate truth tables for the following formulae. Give the conjunctive and disjunctive normal forms of the formulae. Which one of the relations  ,  ,   and   holds?

  1.   whereas   applies.
  2.  

 

Problem 18 (Propositional)Edit

Generate a CNF and a DNF form the following truth table for the formula  .

A B C F
0 0 0 0
1 0 0 1
0 1 0 0
1 0 0 1
1 1 0 1
1 0 1 0
0 1 1 1
1 1 1 0

 

Problem 19 (Propositional)Edit

Generate a CNF from the formula