Page 102 - DCAP310_INTRODUCTION_TO_ARTIFICIAL_INTELLIGENCE_AND_EXPERT_SYSTEMS

Introduction to Artificial Intelligence & Expert Systems

Notes 6.3.1 Properties of WFF

Transforming to Clause Normal Form

There are several algorithms for this conversion, but they all have some parts in common, and
all have similarities. The best algorithm is the one which produces the CNF which is most easily
shown to be unsatisfiable. In general, such a determination is impossible to make, but a common
measure is to aim to produce a CNF with the fewest symbols (where a symbol is a variable,
predicate, or constant). The key feature of all the algorithms is that they are satisfiability
preserving.

The starting point is a set of closed formulae. As a preprocessing step, all variables must be
renamed apart.

Rename Variables Apart

The first operation is to simplify the formulae so that they contain only the ∀, ∃, &, | and ~
connectives. This is done by using known logical identities. The identities are easily verified
using truth tables, to show that the original formula has the same value as the simplified
formula for all possible interpretations of the component formulae, denoted by uppercase
variable letters P and Q.

Simplify
Formula Rewrites to
P <~> Q (P | Q) & (~P | ~Q)
P <=> Q (P => Q) & (Q => P)
P => Q ~P | Q

The second operation is to move negations in so that they apply to only atoms. This is done by
using known logical identities (including De Morgan’s laws), which are easily verified as above.
After moving negations in the formulae are in literal normal form.
Move negations in
Formula Rewrites to
~ X P X ~P
~ X P X ~P
~(P & Q) (~P | ~Q)
~(P | Q) (~P & ~Q)
~~P P

The third operation is to move quantifiers out so that each formula is in the scope of all the
quantifiers in that formula. This is done by using known logical identities, which are easily
verified as above. In these identities, if the variable X already exists in Q, it is renamed to a new
variable name that does not exist in the formula. After moving quantifiers out the formulae are
in prenex normal form.
Move quantifiers out
Formula Rewrites to
X P & Q X (P & Q)
X P & Q X (P & Q)
Contd...

96 LOVELY PROFESSIONAL UNIVERSITY