Logical Representations and

Resolution
 Boolean Logic
Conjunctive normal form
Resolution
 Conjunctive Normal Form
A literal is a variable or a negated variable.
A clause is either a single literal or the disjunction of two or
more literals.
P, P P, and P Q R S are clauses.
(R S ) and P Q are not clauses.

A wff is in conjunctive normal form iff it is either a single

clause or the conjunction of two or more clauses.
(P Q R S) (P R) is in cnf
(P Q R S) (P R) is not in cnf
 Conjunctive Normal Form Theorem
Theorem: Every wff can be converted to an equivalent wff in
conjunctive normal form.
Proof: By construction: conjunctiveBoolean(w: wff) =
1. Eliminate and from w, using the fact that P Q is
equivalent to P Q.
2. Reduce the scope of each to a single term, using the facts:
Double negation: (P) = P
deMorgans laws:
(P Q) (P Q)
(P Q) (P Q)
3. Convert w to a conjunction of clauses using the fact that
both and are associative and the fact that and
distribute over each other.
 Conversion to Conjunctive Normal Form
Let w be the wff :

P (R Q).

Then w can be converted to conjunctive normal form as

follows:

Step 1 produces: P (R Q).

Step 2 produces: P (R Q).

Step 3 produces: (P R) (P Q).

 Resolution

Suppose we know:

winter summer
winter
summer
summer
nil

winter summer
winter cold
summer cold
 Resolution

From the premises: (P Q) and (R Q),

Conclude: (P R).

Resolution is sound: If (P Q) and (R Q) are True, then:

If Q is True, R must be True.

If Q True, P must be True.

Since either Q or Q must be True, P R must be True.

 Resolution The Algorithm

To prove ST from A:

1. Convert A to a list L of clauses in conjunctive normal

form.
2. Construct ST and add it to L.
3. Resolve.
 Complementary Literals
A pair of complementary literals is a pair of literals that are not
mutually satisfiable. So two literals are complementary iff
one is positive, one is negative, and they contain the same
propositional symbol. For example, Q and Q.

Choose two parent clauses that contain a pair of

complementary literals. For example:

C1 = R1 R2 Rj Q
C2 = S1 S2 Sk Q.

Resolve C1 and C2 to derive:

R1 R2 Rj S1 S2 Sk
 Resolution Generating nil

Consider:

Q Q

nil

The empty clause is unsatisfiable since it contains no literals

that can be made True. So if it is ever generated, the
resolution procedure halts and reports that, since adding
ST to A has led to a contradiction, ST is a theorem given
A.
 Resolution The Algorithm
resolve-Boolean(A, ST) =
1. Construct L, the list of of clauses from A.
2. Negate ST, convert the result to conjunctive normal form,
and add the resulting clauses to L.
3. Until either nil is generated or no progress is being made
do:
3. 1 Choose two parent clauses.
3. 2 Resolve the parent clauses together.
3. 3 If the resolvent is not nil and is not in L, add
it to L.
4. If nil was generated, a contradiction has been found.
Return success. ST must be true.
5. If nil was not generated and there was nothing left to do,
return failure.
 Resolution An Example
Prove R given:

Given Axioms: Clauses:

P P
(P Q) R P Q R
(S T) Q S Q
T Q
T T

Add:
R R
 Resolution An Example
P P Q R R
P Q R
S Q
T Q P Q P
T
R
T Q Q

T T

nil
 Resolution Only Select One Pair to Resolve

PQ (1)
P Q R (2)

Prove R:

P Q R R

P Q PQ

? nil

But is R entailed by the two facts we have been given?

 Facts in English
(1) Marcus was a man.

(2) Marcus was a Pompeian.

(3) All Pompeians were Romans.

(4) Caesar was a ruler.

(5) All Romans were either loyal to Caesar or hated him.

(6) Everyone is loyal to someone.

(7) People only try to assassinate rulers they are not loyal to.

(8) Marcus tried to assassinate Caesar.

 An Example - Facts in FOL
(1) Marcus was a man.
man(Marcus)
(2) Marcus was a Pompeian.
Pompeian(Marcus)
(3) All Pompeians were Romans.
x Pompeian(x) Roman(x)
(4) Caesar was a ruler.
ruler(Caesar)
(5) All Romans were either loyal to Caesar or hated him.
x Roman(x) loyalto(x, Caesar) hate(x, Caesar)
(6) Everyone is loyal to someone.
x y loyalto(x, y)
(7) People only try to assassinate rulers they are not loyal to.
x y person(x) ruler(y) tryassassinate(x, y) loyalto(x, y)
(8) Marcus tried to assassinate Caesar.
tryassassinate(Marcus, Caesar)
 Question Answering
(1) Marcus was a man.
man(Marcus)
(2) Marcus was a Pompeian.
Pompeian(Marcus)
(3) All Pompeians were Romans.
x Pompeian(x) Roman(x)
(4) Caesar was a ruler.
ruler(Caesar)
(5) All Romans were either loyal to Caesar or hated him.
x Roman(x) loyalto(x, Caesar) hate(x, Caesar)
(6) Everyone is loyal to someone.
x y loyalto(x, y)
(7) People only try to assassinate rulers they are not loyal to.
x y person(x) ruler(y) tryassassinate(x, y) loyalto(x, y)
(8) Marcus tried to assassinate Caesar.
tryassassinate(Marcus, Caesar)

Was Marcus loyal to Caesar?

 Reasoning Backward
(1) man(Marcus)
(2) Pompeian(Marcus)
(3) x Pompeian(x) Roman(x)
(4) ruler(Caesar)
(5) x Roman(x) loyalto(x, Caesar) hate(x, Caesar)
(6) x y loyalto(x, y)
(7) x y person(x) ruler(y) tryassassinate(x, y) loyalto(x, y)
(8) tryassassinate(Marcus, Caesar)

loyalto(Marcus, Caesar)
(Marcus/x) (Caesar/y)
person(Marcus) ruler(Caesar) tryassassinate(Marcus, Caesar)
 Reasoning Backward
(1) man(Marcus)
(2) Pompeian(Marcus)
(3) x Pompeian(x) Roman(x)
(4) ruler(Caesar)
(5) x Roman(x) loyalto(x, Caesar) hate(x, Caesar)
(6) x y loyalto(x, y)
(7) x y person(x) ruler(y) tryassassinate(x, y) loyalto(x, y)
(8) tryassassinate(Marcus, Caesar)
(9) x man(x) person(x)

loyalto(Marcus, Caesar)
(Marcus/x) (Caesar/y)
person(Marcus) ruler(Caesar) tryassassinate(Marcus, Caesar)
(Marcus/x)
man(Marcus)
 Functions and Predicates
(1) Marcus was a man.
man(Marcus)
(2) Marcus was a Pompeian.
Pompeian(Marcus)
(3) Marcus was born in 40 A.D.
born(Marcus, 40)
(4) All men are mortal.
x man(x) mortal(x)
(5, 6) AllPompeians died when the volcano erupted in 79 A.D.
erupted(volcano, 79) x Pompeian(x) died(x,79)
(7) No mortal lives longer than 150 years.
x t1 t2 mortal(x) born(x, t1) gt(t2-t1, 150) dead(x,t2)
(8) It is now 2004.
now = 2004

Is Marcus alive?
 Functions and Predicates
(1) man(Marcus)
(2) Pompeian(Marcus)
(3) born(Marcus, 40)
(4) x man(x) mortal(x)
(5) erupted(volcano, 79)
(6) x Pompeian(x) died(x,79)
(7) x t1 t2 mortal(x) born(x, t1) gt(t2-t1, 150) dead(x,t2)
(8) now = 2007

alive(Marcus, now)
 Functions and Predicates - Filling in the Blanks
(1) man(Marcus)
(2) Pompeian(Marcus)
(3) born(Marcus, 40)
(4) x man(x) mortal(x)
(5) erupted(volcano, 79)
(6) x Pompeian(x) died(x,79)
(7) x t2 t2 mortal(x) born(x, t1) gt(t2-t1, 150) dead(x,t2)
(8) now = 2007
(9a) x t alive(x, t) dead(x, t)
(9b) x t dead(x,t) alive(x, t)
(10) x t2 t2 died(x, t1) gt(t2, t1) dead(x, t2)

alive(Marcus, now)
 Showing that Marcus is Not Alive
alive(Marcus, now)
(9a) (Marcus/x) (now/t)
dead(Marcus, now)
(10)(Marcus/x)(now/t2) (7) (Marcus/x)(now/t2)

died(Marcus, t1) gt(now, t1) mortal(Marcus) born(Marcus, t1) gt(now-t1,150)

(5) (Marcus/x) (4) (Marcus/x) (3) (40/t1) subst

(79/t1)
Pompeian(Marcus) gt(now, 79) man(Marcus) born(Marcus, 40) gt(now-40,150)

(2) subst (1) subst

T gt(2004, 79) T T gt(2007-40,150)

eval eval

T T
 A Harder One
Given:
x [Roman(x) know(x, Marcus)]
[hate(x, Caesar) (y (z hate(y, z)) thinkcrazy(x, y))]
Roman(Isaac)
hate(Isaac, Caesar)
hate(Paulus, Marcus)
thinkcrazy(Isaac, Paulus)

Prove:
know(Isaac, Marcus)
 Prenex Normal Form
A sentence in first-order logic is in prenex normal form iff it
is of the form:

<quantifier list> <matrix>,

where <quantifier list> is a list of quantified variables and

<matrix> is quantifier-free.

x (y ((P(x) Q(y)) z (R(x, y, z))) is not

in pnf.

x y z (P(x) Q(y)) R(x, y, z) is in pnf. Its matrix is:

(P(x) Q(y)) R(x, y, z).

 Clause Form
A sentence is in clause form iff:

It has been converted to prenex normal form,

Its quantifier list contains only universal quantifiers,
Its quantifier list is no longer explicitly represented,
It is in conjunctive normal form, and
There are no variable names that appear in more than one
clause.

Begin with: x (P(x) Q(x)) y (S(y))

In prenex normal form: x y (P(x) Q(x)) S(y)

In clause form: (P(x) Q(x)) S(y)
 Clause Form Simplifies the Process

x [Roman(x) know(x, Marcus)]

[hate(x, Caesar) (y (z hate(y, z)) thinkcrazy(x, y))]

becomes:

Roman(x) know(x, Marcus) hate(x, Caesar) hate(y, z)

thinkcrazy(x, y)
 Conversion to Clause Form - Step 1
1. Eliminate , using the fact that a b is equivalent to
a b

x [Roman(x) know(x, Marcus)]

[hate(x, Caesar) (y (z hate(y, z)) thinkcrazy(x, y))]

x [Roman(x) know(x, Marcus)]

[hate(x, Caesar) (y (z hate(y, z)) thinkcrazy(x, y))]
 Conversion to Clause Form - Step 2
2. Reduce the scope of each to a single term, using:
(p) = p
deMorgans laws
x P(x) x P(x)
x P(x) x P(x)

x [Roman(x) know(x, Marcus)]

[hate(x, Caesar) (y (z hate(y, z)) thinkcrazy(x, y))]

x [ Roman(x) know(x, Marcus)]

[hate(x, Caesar) (y z hate(y, z) thinkcrazy(x, y))]
 Conversion to Clause Form - Step 3
3. Standardize variables so that each quantifier binds a unique
variable.

x P(x) x Q(x)

x P(x) y Q(y)
 Conversion to Clause Form - Step 4
4. Move all quantifiers to the left without changing their relative
order.

x [ Roman(x) know(x, Marcus)]

[hate(x, Caesar) (y z hate(y, z) thinkcrazy(x, y))]

x y z [ Roman(x) know(x, Marcus)]

[hate(x, Caesar) ( hate(y, z) thinkcrazy(x, y))]

At this point, we have prenex normal form.

 Conversion to Clause Form - Step 5
5. Eliminate existential quantifiers through the use of Skolem
functions and constants.

x Roman(x) Roman(S1)

x z father-of(x, z) x father-of(x, S2(x))

 Conversion to Clause Form - Step 6
6. Drop the prefix since all remaining quantifiers are universal.

x y z [ Roman(x) know(x, Marcus)]

[hate(x, Caesar) ( hate(y, z) thinkcrazy(x, y))]

[ Roman(x) know(x, Marcus)]

[hate(x, Caesar) ( hate(y, z) thinkcrazy(x, y))]
 Conversion to Clause Form - Step 7
7. Convert the matrix into a conjunction of disjuncts by using:
Associative properties of and .
[ Roman(x) know(x, Marcus)]
[hate(x, Caesar) ( hate(y, z) thinkcrazy(x, y))]

Roman(x) know(x, Marcus)

hate(x, Caesar) hate(y, z) thinkcrazy(x, y)

Distributivity of and .

(P(x) Q(x)) T(x)

(P(x) T(x)) (Q(x)) T(x))

 Conversion to Clause Form - Step 8
8. Create a separate clause for each conjunct.

(P(x) T(x)) (Q(x)) T(x))

(P(x) T(x))
(Q(x)) T(x))
 Conversion to Clause Form - Step 9
9. Standardize apart the variables.

(P(x) T(x))
(Q(x)) T(x))

(P(x) T(x))
(Q(y)) T(y))
 Resolution in FOL
To find a contradiction, we must show that the KB, augmented with
P, is unsatisfiable.
Herbrands theorem tells us:
1. To show that a set of clauses S is unsatisfiable, it is necessary to
consider only interpretations over a particular set called the
Herbrand universe of S, which is the set of all ground terms
constructable from the following:
1. The function symbols in S, if any.
2. The constant symbols in S, if any. If none, then the constant
symbol A.
2. A set of clauses S is unsatisfiable iff a finite subset of ground
instances (in which all bound variables have had a value
substituted for them) of S is unsatisfiable.
Resolution is an algorithm that finds contradictions without
enumerating most of the Herbrand universe.
 Unification
In propositional logic, it is easy to identify complementary
literals such as P and P.
But in FOL, what should we do about:
x,y (hate(x, y))
hate(Marcus, Caesar)

Or: hate(Marcus, Caesar)

hate(Paulus, Caesar)

Or: x,y (P(x, x))

P(Marcus, Caesar)
 Before We Start
Before we consider a set of formulas and begin to reason with
them, we need to standardize the variables apart:
Consider:
x, y Lived-In(x, y)
x, y Mother-Of(x, y)

Although we have used x and y in both of these formulas, the

variables in these formulas are logically distinct since they occur
inside the scope of quantifiers that are independent (i.e., neither
lies inside the scope of the other). So an equivalent way to write
these facts is:

x1, y1 Lived-In(x1, y1)

x2, y2 Mother-Of(x2, y2)
 Unification
We need an algorithm that does two things given a sentence S and
a term T:

Determine whether T matches some term T in S, and

Return a substitution that can be applied to the remainder of S.

Example:

S: x,y In(x, y) Climate(y, moderate) Climate(x, moderate)

T: In(Italy, Europe)

The process we will call unification will determine that T matches

the first term of S and it will return the substitution Italy/x,
Europe/y. When we apply that to the remainder of S, we have:

Climate(Europe, moderate) Climate(Italy, moderate)

 The Unification Algorithm
unify-for-resolution(lit1, lit2) =
If either lit1 or lit2 is a variable or a constant then:
Case (checking the conditions in order and executing only the first one that
matches):
lit1 and lit2 are identical: return nil. /* Succeed with no substitution.
lit1 is a variable that occurs in lit2: return Fail. /* These two cases implement the
lit2 is a variable that occurs in lit1: return Fail. occur check.
lit1 is a variable: return (lit2/lit1).
lit2 is a variable: return (lit1/lit2).
otherwise: return Fail. /* No match.
If the initial predicate or function symbols of lit1 and lit2 are not the same, return Fail.
If lit1 and lit2 do not have the same number of arguments, return Fail.
substitution-list = nil.
For i = 1 to the number of arguments of lit1 do
Let S be the result of unify-for-resolution on the ith argument of lit1 and of lit2.
If S contains Fail, return Fail.
If S is not equal to nil then:
Apply S to the remainder of both lit1 and lit2.
Append S to substitution-list.
 The Occur Check
Suppose we are trying to unify: P(x, x)
P(g(x), g(x))

What happens if we skip the occur check?

x and g(x) unify and yield the substitution g(x)/x.

Now we must apply that substitution :

g(x) g(g(x))
g(g(x)) g(g(g(x)))

But if wed standardized apart the variables before we started,

this wouldnt have been a problem.
 The Occur Check is Necessary Even with
Standardizing Apart
Suppose we are trying to unify: P(x, f(x), x)
P(f(a), a, a)

x and f(a) unify and yield the substitution f(a)/x. Applying it:

f(f(a)), f(a)
a, a

Without the occur check, f(f(a)) and a will unify, yielding the
substitution f(f(a))/a. To apply it, we must replace all as in the
remaining terms. But that process never terminates.
 Most General Unifiers (MGUs)
Suppose we are trying to prove x,y (A(x, y) B(x, y))
Using the fact z (A(John, z))
Unifying A(x, y) with A(John, z) yields John/x, z/y. Applying it:
z (B(John, z))
But we could also have matched with the substitution John/x,
John/y, and been left trying to prove B(John, John), which
would be harder.
The algorithm we have presented always returns the most
general unifier. The MGU is unique up to variable name
substitution.
 Unification Examples
Inputs Result Substitution

[1] Roman(x), Succeed Paulus/x

Roman(Paulus)
[2] Roman(x), Fail
Ancient(Paulus)
[3] Roman(father-of(Marcus)), Succeed father-of(Marcus)/x
Roman(x)
[4] Roman(father-of(Marcus)), Fail
Roman(Flavius),
[5] Roman(x), Succeed x/y
Roman(y),
[6] Roman(father-of(x)), Fail (fails occur
Roman(x) check)
[7] Likes(x, y), Succeed Flavius/x, Marcus/y
Likes(Flavius, Marcus)
 FOL Resolution An Example
Prove: Mortal(Marcus) given:

x (Man(x) Mortal(x)) Man(x) Mortal(x)

Man(Marcus) Man(Marcus)

Add: Mortal(Marcus)

Man(x) Mortal(x) Mortal(Marcus)

Marcus/x

Man(Marcus) Man(Marcus)

nil
 FOL Resolution the Algorithm
resolve-FOL(A, ST) =
Construct L, the list of clauses from A.
Rename all variables in ST so that they do not conflict with any variables in L.
Negate ST, convert the result to clause form, and add the resulting clauses to L.
Until either nil is generated or no progress is being made do:
Choose from L two (parent) clauses that contain a pair CL of complementary
literals.
Resolve the parent clauses together to produce a resolvent:
Initially, let the resolvent be the disjunction of all of the literals in both parent
clauses
except for the two literals in CL.
Apply to all of the literals in the resolvent the substitution that was
constructed when
the literals in CL were unified.
Rename all of the variables in the resolvent so that they do not conflict with
any of the
variables in L.
If the resolvent is not nil and is not already in L, add it to L.
If nil was generated, a contradiction has been found. Return success. ST must be true.
If nil was not generated and there was nothing left to do, return failure. ST may or may
not be true. But no proof of ST has been found.
 Heuristics to Aid the Resolution Procedure
Only resolve pairs of clauses that contain complementary
literals.
P(x) Q(x)

Eliminate certain clauses as soon as they are generated:

Tautologies
Clauses that are subsumed by other clauses.

Set of support strategy: whenever possible resolve with a

clause that is part of the statement we are trying to prove.

Unit preference strategy: whenever possible, resolve with

clauses that have a single literal.
 Subsumption
Clause A subsumes clause B iff B must be true in any
interpretation in which A is true. (A is more general than B.)

True

P Q R T W

PQ R T

P Q

PQ

PQW
 Subsumption in FOL
Clause A subsumes clause B iff B must be true in any
interpretation in which A is true. (A is more general than B.)

True

x (P(x))

P(Marcus)

x(P(x))
 Using Resolution
Painter(Leonardo)
Composer(Palistrina)
Country(Italy)
Lived-In(Leonardo, Italy)
In(Italy,Europe)
Climate(Europe, moderate)
Painter(Rubens)
Lived-In(Rubens, Europe)
x,y (In(x, y) Climate(y, moderate) Climate(x, moderate))

Prove that Leonardo was a painter who lived in a moderate climate.

Prove: y (Painter(Leonardo) Lived-In(Leonardo,y) Climate(y, moderate))

Negate it: (y (Painter(Leonardo) Lived-In(Leonardo,y) Climate(y, moderate)))

 Converting to Clause From
Painter(Leonardo)
Composer(Palistrina)
Country(Italy)
Lived-In(Leonardo, Italy)
In(Italy,Europe)
Climate(Europe, moderate)
Painter(Rubens)
Lived-In(Rubens, Europe)

x,y (In(x, y) Climate(y, moderate) Climate(x, moderate))

In(x, y) Climate(y, moderate) Climate(x, moderate)

(y (Painter(Leonardo) Lived-In(Leonardo,y) Climate(y, moderate)))

y ((Painter(Leonardo) Lived-In(Leonardo,y) Climate(y, moderate)))

Painter(Leonardo) Lived-In(Leonardo,y) Climate(y, moderate)

 Using Resolution
1. Painter(Leonardo) 2. Composer(Palistrina)
3. Country(Italy) 4. Lived-In(Leonardo, Italy)
5. In(Italy,Europe) 6. Climate(Europe, moderate)
7. Painter(Rubens) 8. Lived-In(Rubens, Europe)
9. Painter(Sargent)
10. In(x, y) Climate(y, moderate) Climate(x, moderate)

Painter(Leonardo) Lived-In(Leonardo,y) Climate(y, moderate) Painter(Leonardo)

Leonardo/x
Lived-In(Leonardo, Italy) Lived-In(Leonardo,y1) Climate(y1, moderate)

Italy/y1
Climate(Italy, moderate)
 Using Resolution
1. Painter(Leonardo) 2. Composer(Palistrina)
3. Country(Italy) 4. Lived-In(Leonardo, Italy)
5. In(Italy,Europe) 6. Climate(Europe, moderate)
7. Painter(Rubens) 8. Lived-In(Rubens, Europe)
9. Painter(Sargent)
10. In(x, y) Climate(y, moderate) Climate(x, moderate)

Painter(Leonardo) Lived-In(Leonardo,y) Climate(y, moderate) Painter(Leonardo)

Leonardo/x
Lived-In(Leonardo, Italy) Lived-In(Leonardo,y1) Climate(y1, moderate)

Italy/y1
In(x, y) Climate(y, moderate)Climate(x, moderate) Climate(Italy, moderate)

Italy/x
In(Italy,Europe) In(Italy, y2) Climate(y2, moderate)

Europe/y2
Climate(Europe, moderate) Climate(Europe, moderate)
 Answering Questions
A Question: Name a painter who lived in a moderate climate.

?Painter(x) Lived-In(x,y) Climate(y, moderate)

Construct an existence statement to be proved:

x, y (Painter(x) Lived-In(x,y) Climate(y, moderate))

Negate it and resolve, tracking the bindings:

(x, y (Painter(x) Lived-In(x,y) Climate(y, moderate)))

x,y ((Painter(x) Lived-In(x,y) Climate(y, moderate)))
Painter(x) Lived-In(x,y) Climate(y, moderate)
 Tracking the Bindings
Painter(x) Painter(x) Lived-In(x,y) Climate(y, moderate) Painter(Leonardo)

Leonardo/x
Painter(Leonardo) Lived-In(Leonardo,y1) Climate(y1, moderate)

Lived-In(Leonardo, Italy)
Italy/y1

Painter(Leonardo) Climate(Italy, moderate)

In(x, y) Climate(y, moderate)Climate(x, moderate)

Italy/x
In(Italy,Europe) Painter(Leonardo) In(Italy, y2) Climate(y2, moderate)

Europe/y2
Climate(Europe, moderate) Painter(Leonardo) Climate(Europe, moderate)

Painter(Leonardo)
A Reminder About Standardizing Variables Apart
Prove father(Chris, Bill) given:
father(x, y) woman(x) (1)
{father(x, y) woman(x)}
mother(x, y) woman(x) (2)
{mother(x, y) woman(x)}
mother(Chris, Mary) (3)
Add: father(Chris, Bill)

father(x, y) woman(x) mother(x, y) woman(x)

* father(x, y) mother(x, y) mother(Chris, Mary)

Chris/x, Mary/y

father(Chris, Mary)
 Back to Marcus
(1) man(Marcus)
(2) Pompeian(Marcus)
(3) x Pompeian(x) Roman(x)
(4) ruler(Caesar)
(5) x Roman(x) loyalto(x, Caesar) hate(x, Caesar)
(6) x y loyalto(x, y)
(7) x y man(x) ruler(y) tryassassinate(x, y) loyalto(x, y)
(8) tryassassinate(Marcus, Caesar)

(1) man(Marcus)
(2) Pompeian(Marcus)
(3) Pompeian(x1) Roman(x1)
(4) ruler(Caesar)
(5) Roman(x2) loyalto(x2, Caesar) hate(x2, Caesar)
(6) loyalto(x3, S1(x3))
(7) man(x4) ruler(y1) tryassassinate(x4, y1) loyalto(x4, y1)
(8) tryassassinate(Marcus, Caesar)
 Proving Marcus Not Loyal to Caesar
loyalto(M, C) man(x4) ruler(y1) tryassassinate(x4, y1) loyalto(x4, y1)
(M/x4)(C/y1)

man(M) ruler(C) tryassassinate(M,C) man(M)

ruler(C) tryassassinate(M,C) ruler(C)

tryassassinate(M,C) tryassassinate(M,C)

nil
 Does Isaac Know Marcus?
Given:
1. x [Roman(x) know(x, Marcus)]
[hate(x, Caesar) (y (z hate(y, z)) thinkcrazy(x, y))]
Roman(x) know(x, Marcus) hate(x, Caesar)
hate(y, z) thinkcrazy(x, y)

2. Roman(Isaac)
3. hate(Isaac, Caesar)
4. hate(Paulus, Marcus)
5. thinkcrazy(Isaac, Paulus)

Prove:
know(Isaac, Marcus) * know(Isaac, Marcus)
 Does Marcus Hate Caesar?
Try to prove hate(M, C):
Hate(M, C)
Try to Prove that Marcus Does Not Hate Caesar

Try to prove hate(M, C):

Hate(M, C)
Try (Again) to Prove that Marcus Does Not Hate
Caesar
(1) man(Marcus)
(2) Pompeian(Marcus)
(3) Pompeian(x1) Roman(x1)
(4) ruler(Caesar)
(5) Roman(x2) loyalto(x2, Caesar) hate(x2, Caesar)
(6) loyalto(x3, S1(x3))
(7) man(x4) ruler(y1) tryassassinate(x4, y1) loyalto(x4, y1)
(8) tryassassinate(Marcus, Caesar)
(9) persecute(x5, y2) hate(y2, x5) persecute(x, y) hate(y, x)
(10) hate(x6, y3) persecute(y3, x6) hate(x, y) persecute(y, x)

Now try to prove hate(M, C):

Hate(M, C)
 A Winnie Example

"And if anyone knows anything about anything," said Bear to

himself,
"It's Owl who knows something about something," he said,
"Or my name
is not Winnie-the-Pooh," he said. "Which it is," he added.
"So there you are."
 When Does Resolution Work?
Resolution is sound and refutation-complete.
If there is a contradiction, resolution will eventually find it if
resolvents are chosen systematically.
But:
It may take exponential time.
Satisfiability is semi-decidable: if a set of clauses is satisfiable,
resolution will never find a conflict and it may not notice that it
is failing to do so.
 Satisfiability is Semi Decidable
Suppose we want to know whether P(x) is true. There are
three possibilities:
(1) P(x) is entailed by KB and thus:
P(x) KB is unsatisfiable.
(2) P(x) is entailed by KB and thus:
P(x) KB is unsatisfiable.
(3)
 Horn Clauses

A Horn Clause is a clause in which at most one literal is

positive.
A(x) B(x) C(x) becomes
A(x) B(x) C(x) a Horn clause
Deciding entailment with Horn clauses can be done in time
that is linear in the size of the KB by using either backward or
forward chaining.