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.
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:
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.
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
The binary junctor for exclusive disjunction is
defined by . Show that the
following holds for propositional logic formulae , and :
- (Commutativity).
- (Associativity)
Show the following by equivalence transformation. Give to all remodelling steps the used rules!
Prove with equivalences:
- is a tautology.
- is unsatisfiable.
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 .
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 .
The following formulae are given:
- Simplify by using .
- Simplify by using equivalences but not .
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
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.
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.
Create formulae in (a) conjunctive or (b) disjunctive normal form which are equivalent to:
where denotes exclusive or.
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?
Generate truth tables for the following formulae.
Give the conjunctive and disjunctive normal forms of the
formulae. Which one of the relations , , and holds?
- whereas applies.
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
|
Generate a CNF from the formula