Page 104 - DCAP310_INTRODUCTION_TO_ARTIFICIAL_INTELLIGENCE_AND_EXPERT_SYSTEMS

Introduction to Artificial Intelligence & Expert Systems

Notes Skolemize
∃X ((~taller(Y,X) & ~wise(X)) | wise(Y)) ã = {Y}
(~taller(Y,x(Y)) & ~wise(x(Y))) | wise(Y)

Distribute disjunctions
(~taller(Y,x(Y)) | wise(Y)) & (~wise(x(Y)) | wise(Y))
Convert to CNF
{ ~taller(Y,x(Y)) | wise(Y),
~wise(x(Y)) | wise(Y) }

!

Caution Use of truth table should be handled carefully.

Task Find the effect of propositional logic in real life.

Self Assessment

State whether the following statements are true or false:
5. A formula is a syntactic formal object that can be informally given a semantic meaning.
6. A formal language may thus have an infinite number of formulas regardless whether each
formula has a token instance.

6.4 Conversion to Clausal Form

Clause Normal Form (CNF)

Clause Normal Form is a sub-language of 1st order logic. A clause is an expression of the form
L |... | L where each L is a literal. Clauses are denoted by uppercase letters with a superscript
1 m i
|
|, e.g., C . There are satisfiability preserving transformations from 1st order logic to CNF, i.e.,
if a set of (1st order) formulae are satisfiable, then their CNF is satisfiable. Conversely, if the
CNF of a set of formulae is unsatisfiable, then the formulae are unsatisfiable. This is then useful
for showing logical consequence. The benefit of converting to CNF is that more is possible
using just the Herbrand interpretations. Computationally, CNF is easier to work with, and is
the form used by the resolution inference rule.

6.4.1 Conversion to Clausal Normal Form

Clauses may be expressed in Kowalski form. Kowalski form forms the antecedent of an
implication by conjoining the atoms of the negative literals in a clause, and forms the consequent
from the disjunction of the positive literals.

Example 1:
~taller(Y,x(Y)) | wise(Y) | ~wise(x(Y)) | taller(x(Y),Y)
is written as
taller(Y,x(Y)) & wise(x(Y)) => wise(Y) | taller(x(Y),Y)

If the antecedent is empty it is set to TRUE, and if the consequent is empty it is set to FALSE.

98 LOVELY PROFESSIONAL UNIVERSITY