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

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Propositional Logic
Jump to: navigation, search

Equivalence and Normal Forms[edit]

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 6[edit]

The formulae F and G are called (semantically) equivalent, iff for all assignments \mathcal{A} for F and G, \mathcal{A}(F)= \mathcal{A}(G). We write F \equiv G.

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

Theorem 3 (Substituitivity)[edit]

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

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

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

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

Theorem 4[edit]

The following equivalences hold:

(F \land F) \equiv F

(F \lor F) \equiv F (Idempotence)

(F \land G) \equiv (G \land F)

(F \lor G) \equiv (G \lor F) (Commutativity)

((F \land G) \land H) \equiv (F \land (G \land
       H))

((F \lor G) \lor H) \equiv (F \lor (G \lor H)) (Associativity)

(F \land (F \lor G)) \equiv F

(F \lor (F \land G)) \equiv F (Absorption)

(F \land (G \lor H)) \equiv ((F \land G) \lor (F
       \land H))

(F \lor (G \land H)) \equiv ((F \lor G) \land (F
\lor H)) (Distributivity)

\lnot ~\lnot F \equiv F (Double negation)

\lnot(F \land G) \equiv (\lnot F \lor \lnot G)

\lnot(F \lor G) \equiv (\lnot F \land \lnot G) (deMorgan's rule)

(F \lor G) \equiv F, if F is a tautology

(F \land G) \equiv G, if F is a tautology (Rule of Tautology)

(F \lor G) \equiv G, if F is unsatisfiable

(F \land G) \equiv F, if F is unsatisfiable (Rule of Unsatisfiability)


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

F G (F\land G) (F \lor (F \land G))
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:


((A\lor (B\lor C)) \land (C \lor \lnot A))\equiv  ((B \land \lnot A) \lor C)



((A \lor (B \lor C)) \land (C \lor \lnot A))


\equiv ((A \lor B) \lor C) \land (C \lor \lnot A)) Associativity and TS

\equiv ((C \lor (A \lor B)) \land ((C \lor \lnot A)) Commutativity and TS

\equiv (C \lor ((A \lor B) \land \lnot A)) Distributivity

\equiv (C \lor (\lnot A \land (A \lor B))) Commutativity and TS

\equiv (C \lor ((\lnot A \land A) \lor (\lnot A \land B)) Distributivity and TS

\equiv (C \lor (\lnot A \land B)) Unsatisfiability and TS

\equiv (C \lor (B \land \lnot A)) Commutativity and TS

\equiv ((B \land \lnot A) \lor C) Commutativity and TS


Problems[edit]

Problem 9 (Propositional)[edit]

The binary junctor \stackrel{\cdot} \vee for exclusive disjunction is defined by  F \stackrel{\cdot} \vee G = F \leftrightarrow (\lnot G). Show that the following holds for propositional logic formulae F, G and H:

  1. F \stackrel{\cdot} \vee G \equiv G \stackrel{\cdot} \vee F (Commutativity).

  2. (F \stackrel{\cdot} \vee G) \stackrel{\cdot} \vee H \equiv F \stackrel{\cdot} \vee (G \stackrel{\cdot} \vee H) (Associativity)


\Box

Problem 10 (Propositional)[edit]

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

  1. (A \to (B \lor C)) \equiv (A \to B) \lor (A \to C)
  2. (A \to B) \to A \equiv (B \to A) \land (B \lor A)
  3. A \leftrightarrow \lnot B \equiv \lnot (A \leftrightarrow B)
  4. (A \to (B \land C)) \equiv (A \to B) \land (A \to C)
  5. (A \to B) \to (B \to A) \equiv B \to A
  6. (A \lor \lnot B) \lor ((\lnot A \land \lnot C) \land B)\equiv (A \lor \lnot C) \lor \lnot B


\Box

Problem 11 (Propositional)[edit]

Prove with equivalences:

  1. p \lor \lnot(p \land q) is a tautology.
  2. (p \lor \lnot q) \land (\lnot p \land q) is unsatisfiable.


\Box

Problem 12 (Propositional)[edit]

The binary junctor \downarrow with the meaning neither-nor is defined by F \downarrow G = \lnot(F \lor G). Let F be a propositional logic formula, which contains only the operators \land \lor and \lnot. Prove that for every formula F a formula  \mathcal{T} (F) exists, such that F \equiv \mathcal{T} (F) and \mathcal{T} (F) is built by using only the junctor \downarrow.


\Box

Problem 13 (Propositional)[edit]

Let F be a propositional logic formula, which contains only the operators \land, \lor and \lnot. Prove that for every formula F a formula \mathcal{T}(F) exists, such that F \equiv \mathcal{T}(F) and \mathcal{T}(F) is built by using only the junctors \to and \stackrel{\cdot} \vee.

\Box

Problem 14 (Propositional)[edit]

The following formulae are given:

  • A \equiv D \lor B
  • B \equiv \lnot B \lor \lnot D \lor \lnot S
  • C \equiv (\lnot S\land D) \lor \lnot B



  1. Simplify A \land B \land C by using B \land C \equiv C.
  2. Simplify A \land B \land C by using equivalences but not B \land C \equiv C.


\Box

Definition 7 (Normal Forms)[edit]

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


F = (\bigwedge^n_{i=1} (\bigvee^{m_i}_{j=1}  L_{i,j}))

where L_{ij} is a literal.


A formula F is in disjunctive normalform (DNF) iff

F = (\bigvee^n_{i=1} (\bigwedge^{m_i}_{j=1} L_{i,j}))

where L_{ij} is a literal

Theorem 5[edit]

For every formula F 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 F


1. Substitute in F every subformula of the form

\lnot ~\lnot ~G \text{ by }  G
\lnot ~(G ~\land ~H)   \text{ by }   (\lnot ~G ~\lor ~\lnot ~H)
\lnot ~(G ~\lor ~H) \text{ by }  (\lnot ~G ~\land ~\lnot ~H)

until there is no subformula of this kind.

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

(F ~\lor ~(G~\land~H))   \text{ by }   ((F~\lor~G) ~\land ~(F~\lor~H))
((F~\land~G) ~\lor ~H) \text{ by } ((F~\lor~H) ~\land ~(G~\lor~H))

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 F, 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 F, we have to take into account, that every line of the table which yields the truthvalue true gives one conjunction: if the assignment of the literal A_i is true it is included as  \ldots \land A_i \land  \ldots, if is false we include \ldots \land \lnot A_i \ldots \land \ldots. For the above example we get as a DNF:

(\lnot A  \land  \lnot  B\land  \lnot C )  \lor

( A  \land  \lnot  B\land  \lnot C )   \lor

( A  \land  \lnot  B\land      C )


If we change in the above procedure the roles of true and false and \lor and \land we arrive at a CNF:

( A \lor B \lor\lnot C)  \land

(A\lor\lnot B\lor C) \land

(A \lor  \lnot B \lor \lnot C) \land

( \lnot A \lor \lnot B \lor C) \land

(\lnot A \lor \lnot B \lor \lnot C)


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 F_i of a conjunction F_1, \cdots , F_l is written as:


A_1 \land  \cdots \land A_n \to B_1 \lor \cdots \lor B_m

It is easy to see, that this implication is logically equivalent to a disjunction \lnot A_1 \lor \cdots \lor  \lnot A_n \lor B_1 \lor \cdots \lor B_m. Sometimes the implication is written as


A_1,  \cdots , A_n \to B_1; \cdots ; B_m

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:


A_1,  \cdots , A_n \to B_1, \cdots , B_m

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 8[edit]

If F is a formula in CNF, i.e.

 F = (L_{1,1} \lor \ldots \lor L_{1,{n_1}}) \land
\ldots \land (L_{k,1} \lor \ldots \lor L_{k,{n_k}})

then its corresponding representation in clause form is given as

 F = \{ \{L_{1,1}, \ldots, L_{1,{n_1}}\}, 
\ldots , \{L_{k,1}, \ldots, L_{k,{n_k}}\} \}

The sets \{L_{i,1}, \ldots, L_{i,{n_i}}\} 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.

 ( (A_1 \lor \lnot A_2) \land (A_3 \land A_3) )             \{\{A_1, \lnot A_2\}, \{A_3\}\}


(A_3 \land (\lnot A_2 \lor A_1))

Problems[edit]

Problem 15 (Propositional)[edit]

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

 A \stackrel{\cdot} \vee B \stackrel{\cdot} \vee C


where \stackrel{\cdot} \vee denotes exclusive or.


\Box

Problem 16 (Propositional)[edit]

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

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

Which laws of the logic justify these procedures?

\Box

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 F \models G, G \models F, F \equiv G and F = G holds?

  1. F = (A \land \lnot (B \lor C)) \stackrel{\cdot} \vee ((A \to B) \lor (A \to C),) whereas F \stackrel{\cdot} \vee G = F \leftrightarrow (\lnot G) applies.
  2. G = ((A \lor (B \land A)) \to \lnot A) \lor C

\Box

Problem 18 (Propositional)[edit]

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

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

\Box

Problem 19 (Propositional)[edit]

Generate a CNF from the formula (P \land(Q \to R)\to  S)

\Box