Page 103 - DCAP310_INTRODUCTION_TO_ARTIFICIAL_INTELLIGENCE_AND_EXPERT_SYSTEMS

Unit 6: Formalized Symbolic Logics

Q & X P X (Q & P) Notes
Q & X P X (Q & P)
X P | Q X (P | Q)
X P | Q X (P | Q)
Q | X P X (Q | P)
Q | XP X (Q | P)
The fourth operation is to skolemize to remove existential quantifiers. This step replaces
existentially quantified variables by skolem functions and removes all quantifiers. The variables
remaining after skolemization are all implicitly universally quantified. Whereas the previous
three operations maintain equivalence between the original and transformed formulae,
skolemization does not. However, Skolemization does maintain the satisfiability of the formulae,
which is what is required for the overall goal of establishing logical consequence. After
Skolemization the formulae are in Skolem normal form.
Skolemize
Formula Rewrites to
Initially Set γ = {}
X P P
and set γ = γ {X}
X P P[X/x(γ)]
where x is a new Skolem functor.
The fifth operation is to distribute disjunctions so that the formulae are conjunctions of
disjunctions. This is done by using known logical identities, which are easily verified as above.
After distributing disjunctions the formulae are in conjunctive normal form.

Distribute Disjunctions
Formula Rewrites to
P | (Q & R) (P | Q) & (P | R)
(Q & R) | P (Q | P) & (R | P)

The last operation is to convert to Clause Normal Form. This is done by removing the
conjunctions, to form a set of clauses.

Convert to CNF
Formula Rewrites to
P 1 & ... & P n {P 1,...,P n}

Example:
1st order formula
∀Y (∀X (taller(Y,X) | wise(X)) => wise(Y))

Simplify
∀Y (~∀X (taller(Y,X) | wise(X)) | wise(Y))
Move negations in
∀Y (∃X (~taller(Y,X) & ~wise(X)) | wise(Y))
Move quantifiers out
∀Y (∃X ((~taller(Y,X) & ~wise(X)) | wise(Y)))

LOVELY PROFESSIONAL UNIVERSITY 97