Predicate logic

REPRESENTING SIMPLE FACTS IN LOGIC

 Socrates is a man.
We could write:
SOCRATESMAN
But if we also wanted to represent
Plato is a man.
we would have to write something such as:
PLATOMAN
which would be a totally separate assertion, and we would not be able to draw any conclusions about
similarities between Socrates and Plato.

It would be much better to represent these facts as:

MAN(SOCRATES)
MAN(PLATO)
since now the structure of the representation reflects the structure of the knowledge itself. But to do
that, we need to be able to use predicates applied to arguments. We are in even more difficulty if we
try to represent the equally classic sentence
All men are mortal.
We could represent this as:
MORTALMAN

But that fails to capture the relationship between any individual being a man and that
individual being a mortal. To do that, we really need variables and quantification unless we are willing
to write separate statements about the mortality of every known man.
 Let's now explore the use of predicate logic as a way of representing
knowledge by looking at a specific example. Consider the following set of
sentences:
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.
The facts described by these sentences can be represented as a set of wff's in predicate logic as
follows:
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) V hate(x, Caesar)
6. Everyone is loyal to someone.
∀x : ∃ y : Ioyalto(x,y)
7. People only try to assassinate rulers they are not loyal to.
∀ x : ∀ y : person(x) ∧ ruler(y) ∧ tryassassinate(x,y) → ¬ Ioyalto(x,y)
8. Marcus tried to assassinate Caesar.
tryassassinate (Marcus, Caesar)
9. All men are people.
∀x : man(x) → person(x)
Now suppose that we want to use these statements to answer the question
Was Marcus loyal to Caesar?
 The next example shows how these ideas of computable functions and predicates
can be useful. Consider the following set of facts, again involving Marcus:
I. 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. All Pompeians died when the volcano erupted in 79 A.D.
erupted(volcano, 79) ∧ ∀ x : *Pompeian(x) → died(x, 79)+
6. No mortal lives longer than 150 years.
∀x: ∀t1: At2: mortal(x) ∧ born(x, t1) ∧ gt(t2 - t1,150) → dead(x, t2)
7. It is now 1991.
now = 1991
8. Alive means not dead.
∀x: ∀t: *alive(x, t) → ¬ dead(x,t)] ∧ *¬ dead(x, t) → alive(x, t)+
9. If someone dies, then he is dead at all later times.
∀x: ∀t1: At2: died(x, t1) ∧ gt(t2, t1) → dead(x, t2)
Now let's attempt to answer the question "Is Marcus alive?" by proving:
¬ alive(Marcus, now)
Conversion to Clause form
Suppose we know that all Romans who know Marcus either hate Caesar or
think that anyone who hates anyone is crazy. We could represent that in the
following wff:

∀x: [Roman(x) ∧ know(x, Marcus)+ →

[hate(x, Caesar) V (∀y : ∃z : hate (y, z) → thinkcrazy(x, y))+

The formula given above would be represented in conjunctive normal form

as:

¬ Roman(x) ∧ ¬ know(x, Marcus) V

hate(x, Caesar) V ¬ hate(y, z) V thinkcrazy(x, z)
Algorithm: Convert to Clause Form

1. Eliminate →, using the fact that a → b is equivalent to ¬ a V b.

Performing this transformation on the wff given above yields

∀x: ¬ [Roman(x) ∧ know(x, Marcus)] V

[hate(x, Caesar) V (∀y : ¬(∃z : hate(y, z)) V thinkcrazy(x, y))]

2. Reduce the scope of each ¬ to a single term, using the fact that ¬ (¬ p) = p,
deMorgan's laws [which say that ¬ (a ∧ b) = ¬ a V ¬ b and ¬ (a V b) = ¬ a ∧ ¬ b
], and the standard correspondences between quantifiers [¬ ∀x: P(x) = ∃x: ¬
P(x) and ¬ ∃x: P(x) = ∀ x: ¬P(x)]. Performing this transformation on the wff
from step 1 yields

∀x: [¬ Roman(x) V ¬ know(x, Marcus)] V

[hate(x, Caesar) V (∀y: ∀z: ¬ hate(y, z) V thinkcrazy(x, y))]
3. Standardize variables so that each quantifier binds a unique variable. Since
variables are just dummy names, this process cannot affect the truth value of
the wff. For example, the formula
∀x: P(x) V ∀x: Q(x)
would be converted to
∀x: P(x) V ∀y: Q(y)

4. Move all quantifiers to the left of the formula without changing their
relative order. This is possible since there is no conflict among variable names.
Performing this operation on the formula of step 2, we get

∀x: ∀y: ∀z: [¬ Roman(x) V ¬ know(x, Marcus)] V

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

At this point, the formula is in what is known as prenex normal form. It

consists of a prefix of quantifiers followed by a matrix, which is quantifier-
free.
5. Eliminate existential quantifiers. A formula that contains an existentially quantified
variable asserts that there is a value that can be substituted for the variable that
makes the formula true. We can eliminate the quantifier by substituting for the
variable a reference to a function that produces the desired value. Since we do not
necessarily know how to produce the value, we must create a new function name for
every such replacement. We make no assertions about these functions except that
they must exist. So, for example, the formula
∃y : President(y)
can be transformed into the formula
President(S1)
where S1 is a function with no arguments that somehow produces a value that
satisfies President. If existential quantifiers occur within the scope of universal
quantifiers, then the value that satisfies the predicate may depend on the values of
the universally quantified variables. For example, in the formula
∀x: ∃y: father-of(y, x)
the value of y that satisfies father-of depends on the particular value of x. Thus we
must generate functions with the same number of arguments as the number of
universal quantifiers in whose scope the expression occurs. So this example would be
transformed into
∀x: father-of(S2(x), x)
These generated functions are called Skolem functions. Sometimes ones with no
arguments are called Skolem constants.
6. Drop the prefix. At this point, all remaining variables are universally quantified, so the prefix can just
be dropped and any proof procedure we use can simply assume that any variable it sees is universally
quantified. Now the formula produced in step 4 appears as
[¬ Roman(x) V ¬ know(x, Marcus)] V
[hate(x, Caesar) V (¬ hate(y, z) V thinkcrazy(x, y))]

7. Convert the matrix into a conjunction of disjuncts. In the case or our example, since there are no
and’s, it is only necessary to exploit the associative property of or [ i.e., (a ∧ b) V c = (a V c) ∧ (b ∧ c)] and
simply remove the parentheses, giving
¬ Roman(x) V ¬ know(x, Marcus) V
hate(x, Caesar) V ¬ hate(y, z) V thinkcrazy(x, y)

However, it is also frequently necessary to exploit the distributive property [i.e. , (a ∧ b) V c = (a V c) ∧ (b

V c)]. For example, the formula
(winter ∧ wearingboots) V (summer ∧ wearingsandals)
becomes, after one application of the rule
[winter V (summer ∧ wearingsandals)]
∧ [wearingboots V (summer ∧ wearingsandals)]
and then, after a second application, required since there are still conjuncts joined by OR's,
(winter V summer) ∧
(winter V wearingsandals) ∧
(wearingboots V summer) ∧
(wearingboots V wearingsandals)
8. Create a separate clause corresponding to each conjunct. In order for a wff to be
true, all the clauses that are generated from it must be true. If we are going to be
working with several wff’s, all the clauses generated by each of them can now be
combined to represent the same set of facts as were represented by the original wff's.

9. Standardize apart the variables in the set of clauses generated in step 8. By this we
mean rename the variables so that no two clauses make reference to the same
variable. In making this transformation, we rely on the fact that
(∀x: P(x) ∧ Q(x)) = ∀x: P(x) ∧ ∀x: Q(x)
Thus since each clause is a separate conjunct and since all the variables are
universally quantified,
there need be no relationship between the variables of two clauses, even if they
were generated
from the same wff.
 Resolution in Propositional Logic
In order to make it clear how resolution works, we first present the resolution procedure for
propositional logic. We then expand it to include predicate logic.
In propositional logic, the procedure for producing a proof by resolution of proposition P
with respect to a set of axioms F is the following.
Algorithm: Propositional Resolution
1 . Convert all the propositions of F to clause form.
2. Negate P and convert the result to clause form. Add it to the set of clauses obtained in step 1.
3. Repeat until either a contradiction is found or no progress can be made:
(a) Select two clauses. Call these the parent clauses.
(b) Resolve them together. The resulting clause, called the resolvent, will be the disjunction of all of
the literals of both of the parent clauses with the following exception: If there are any pairs of literals
L and ¬ L such that one of the parent clauses contains L and the other contains ¬ L, then select one
such pair and eliminate both L and ¬ L from the resolvent.
(c) If the resolvent is the empty clause, then a contradiction has been found. If it is not, then add it to
the set of clauses available to the procedure.
 Let's look at a simple example. Suppose we are given the axioms
shown in the first column of Fig. 5.7 and we want to prove R. First we convert
the axioms to clause form, as shown in the second column of the figure.

Then we negate R, producing ¬ R, which is already in clause form.

The Unification Algorithm
• In propositional logic, it is easy to determine that two literals cannot both be true
at the same time.
• For example, man(John) and ¬ man(John) is a contradiction, while man(John) and ¬
man(Spot) is not.
• Thus, in order to determine contradictions, we need a matching procedure that
compares two literals and discovers whether there exists a set of substitutions that
makes them identical.
• There is a straightforward recursive procedure, called the unification algorithm,
that does just this.
• To attempt to unify two literals, we first check if their initial predicate symbols are
the same. If so, we can proceed. Otherwise, there is no way they can be unified,
regardless of their arguments. For example, the two literals cannot be unified.
tryassassinate (Marcus, Caesar)
hate(Marcus, Caesar)
 If the predicate symbols match, then we must check the arguments,
one pair at a time. If the first matches, we can continue with the second, and
so on. To test each argument pair, we can simply call the unification
procedure recursively. The matching rules are simple. Different constants or
predicates cannot match; identical ones can. A variable can match another
variable, any constant, or a predicate expression, with the restriction that the
predicate expression must not contain any instances of the variable being
matched.

The only complication in this procedure is that we must find a single,

consistent substitution for the entire literal , not separate ones for each piece
of it. To do this, we must take each substitution that we find and apply it to
the remainder of the literals before we continue trying to unify them
For example, suppose we want to unify the expressions
P(x, x)
P(y, z)
The two instances of P match fine. Next we compare x and y, and decide that if we
substitute y for x, they could match. We will write that substitution as
y/x
(We could, of course, have decided instead to substitute x for y, since they
are both just dummy variable names. The algorithm will simply pick one of these two
substitutions.) But now, if we simply continue and match x and z, we produce the
substitution z/x. But we cannot substitute both y and z for x, so we have not produced
a consistent substitution.
What we need to do after finding the first substitution y/x is to make that
substitution throughout the literals, giving
P(y, y)
P(y, z)
 Now we can attempt to unify arguments y and z, which succeeds with the substitution z/y.
The entire unification process has now succeeded with a substitution that is the composition of the two
substitutions we found. We write the composition as
(z/y)(y/x)
following standard notation for function composition. In general, the substitution (a1/a2, a3/a4,
…)(b1/b2, b3/b4, …)… means to apply all the substitutions of the right- most list, then take the result
and apply all the ones of the next list, and so forth, until all substitutions have been applied.
The object of the unification procedure is to discover at least one substitution that causes
two literals to match. Usually, if there is one such substitution there are many. For example, the literals
hate(x, y)
hate(Marcus, z)
could be unified with any of the following substitutions:
(Marcus/x, z/y)
(Marcus/x, y/z)
(Marcus/x, Caesar/y, Caesar/z)
(Marcus/x, Polonius/y, Polonius/z)
The first two of these are equivalent except for lexical variation. But the second two, although they
produce a match, also produce a substitution that is more restrictive than absolutely necessary for the
match. Because the final substitution produced by the unification process will be used by the resolution
procedure, it is useful to generate the most general unifier possible. The algorithm shown below will do
that.
Having explained the operation of the unification algorithm, we can now state it concisely.
We describe a procedure Unify(L1 , L2), which returns as its value a list representing the composition of
the substitutions that were performed during the match.
The empty list, NIL, indicates that a match was found without any substitutions. The list consisting of the
single value FAIL indicates that the unification procedure failed.
Algorithm: Unify(L1, L2)
I. If L1 or L2 are both variables or constants, then:
(a) If L1 and L2 are identical, then return NIL.
(b) Else if L1 is a variable, then if L1 occurs in L2 then return {FAIL}, else return (L2/L1).
(c) Else if L2 is a variable, then if L2 occurs in L1 then return {FAIL} , else return (L1/L2).
(d) Else return {FAIL}.
2. If the initial predicate symbols in L1 and L2 are not identical, then return {FAIL}.
3. If LI and L2 have a different number of arguments, then return {FAIL}.
4. Set SUBST to NIL. (At the end of this procedure, SUBST will contain all the substitutions used to unify
L1 and L2.)
5. For i ← 1 to number of arguments in L1 :
(a) Call Unify with the ith argument of L1 and the ith argument of L2, putting result in S.
(b) If S contains FAIL then return {FAIL}.
(c) If S is not equal to NIL then:
(i) Apply S to the remainder of both L1 and L2.
(ii) SUBST: = APPEND(S, SUBST).
6. Return SUBST.
The only part of this algorithm that we have not yet discussed is the check in steps 1(b) and
1(c) to make sure that an expression involving a given variable is not unified with that variable.
Suppose we were attempting to unify the expressions
f(x, x)
f(g(x),g(x))
If we accepted g(x) as a substitution for x, then we would have to substitute it for x in the remainder of
the expressions. But this leads to infinite recursion since it will never be possible to eliminate x.
Unification has deep mathematical roots and is a useful operation in many AI programs, for
example, theorem provers and natural language parsers. As a result, efficient data structures and
algorithms for unification have been developed. For an introduction to these techniques and
applications, see Knight [1989].
Resolution in Predicate Logic
We now have an easy way of determining that two literals are contradictory- they are if one of them can
be unified with the negation of the other. So, for example, man(x) and ¬ man(Spot) are contradictory,
since man(x) and man(Spot) can be unified. This corresponds to the intuition that says that man(x)
cannot be true for all x if there is known to be some x, say Spot, for which man(x) is false. Thus in order
to use resolution for expressions in the predicate logic, we use the unification algorithm to locate pairs
of literals that cancel out.
We also need to use the unifier produced by the unification algorithm to generate the
resolvent clause. For example. suppose we want to resolve two clauses:
1. man(Marcus)
2. ¬ man(x1) V mortal(x1)
The literal man(Marcus) can be unified with the literal man(x1) with the substitution Marcus/x1, telling
us that for x1 = Marcus, ¬ man(Marcus) is false. But we cannot simply cancel out the two man literals as
we did in propositional logic and generate the resolvent mortal(x1). Clause 2 says that for a given x1,
either ¬ man(x1) or mortal(x1). So for it to be true, we can now conclude only that mortal(Marcus) must
be true.
It is not necessary that mortal(x1) be true for all x1 since for some values of x1, ¬ man(x1) might be
true, making mortal(x1) irrelevant to the truth of the complete clause. So the resolvent generated by
clauses 1 and 2 must be mortal(Marcus), which we get by applying the result of the unification process
to the resolvent. The resolution process can then proceed from there to discover whether
mortal(Marcus) leads to a contradiction with other available clauses.
This example illustrates the importance of standardizing variables apart during the process
of converting expressions to clause form. Given that that standardization has been done, it is easy to
determine how the unifier must be used to perform substitutions to create the resolvent. If two
instances of the same variable occur then they must be given identical substitutions.
We can now state the resolution algorithm for predicate logic as follows, assuming a set of
given statements F and a statement to be proved P:
Algorithm: Resolution
1. Convert all the statements of F to clause form.
2. Negate P and convert the result to clause form. Add it to the set of clauses obtained in 1.
3. Repeat until either a contradiction is found , no progress can be made, or a predetermined amount of
effort has been expended.
(a) Select two clauses. Call these the parent clauses.
(b) Resolve them together. The resolvent will be the disjunction of all the literals of both parent
clauses with appropriate substitutions performed and with the following exception: If there is one
pair of literals T1 and ¬ T2 such that one of the parent clauses contains T2 and the other contains T1
and if T1 and T2 are unifiable, then neither T1 nor T2 should appear in the resolvent. We call T1 and
T2 Complementary literals. Use the substitution produced by the unification to create the resolvent.
If there is more than one pair of complementary literals, only one pair should be omitted from the
resolvent.
 (c) If the resolvent is the empty clause, then a contradiction has been found. If it is not, then add it to
the set of clauses available to the procedure.
If the choice of clauses to resolve together at each step is made in certain systematic ways,
then the resolution procedure will find a contradiction if one exists. However, it may take a very long
time. There exist strategies for making the choice that can speed up the process considerably:
• Only resolve pairs of clauses that contain complementary literals, since only such resolutions produce
new clauses that are harder to satisfy than their parents. To facilitate this, index clauses by the
predicates they contain, combined with an indication of whether the predicate is negated. Then, given a
particular clause, possible resolvents that contain a complementary occurrence of one of its predicates
can be located directly.
• Eliminate certain clauses as soon as they are generated so that they cannot participate in later
resolutions. Two kinds of clauses should be eliminated: tautologies (which can never be unsatisfied) and
clauses that are subsumed by other clauses (i.e., they are easier to satisfy. For example, P V Q is
subsumed by P.)
• Whenever possible, resolve either with one of the clauses that is part of the statement we are trying
to refute or with a clause generated by a resolution with such a clause. This is called the set-of-support
strategy and corresponds to the intuition that the contradiction we are looking for must involve the
statement we are trying to prove. Any other contradiction would say that the previously believed
statements were inconsistent.
• Whenever possible, resolve with clauses that have a single literal. Such resolutions generate new
clauses with fewer literals than the larger of their parent clauses and thus are probably closer to the
goal of a resolvent with zero terms. This method is called the unit-preference strategy.
Let's now return to our discussion of Marcus and show how resolution can be used to prove
new things about him. Let's first consider the set of statements introduced in Section 5. 1. To use them
in resolution proofs, we must convert them to clause form as described in Section 5.4.1. Figure 5.9(a)
shows the results of that conversion. Figure 5.9(b) shows a resolution proof of the statement.
The facts described by these sentences can be represented as a set of wff's in predicate logic as
follows:
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) V hate(x, Caesar)
6. Everyone is loyal to someone.
∀x : ∃ y : Ioyalto(x,y)
7. People only try to assassinate rulers they are not loyal to.
∀ x : ∀ y : person(x) ∧ ruler(y) ∧ tryassassinate(x,y) → ¬ Ioyalto(x,y)
8. Marcus tried to assassinate Caesar.
tryassassinate (Marcus, Caesar)
Question Answering
Very early in the history of AI it was realized that theorem-proving techniques could be applied to the
problem of answering questions. As we have already suggested, this seems natural since both deriving
theorems from axioms and deriving new facts (answers) from old facts employ the process of
deduction. We have already shown how resolution can be used to answer yes-no questions, such as "Is
Marcus alive?" In this section, we show how resolution can be used to answer fill-in-the-blank
questions, such as "When did Marcus die?" or "Who tried to assassinate a ruler?” Answering these
questions involves finding a known statement that matches the terms given in the question and then
responding with another piece of the same statement that fills the slot demanded by the question. For
example, to answer the question "When did Marcus die?" we need a statement of the form
died(Marcus, ??)
with ?? actually filled in by some particular year. So, since we can prove the statement
died(Marcus, 79)
we can respond with the answer 79.
It turns out that the resolution procedure provides an easy way of locating just the statement we
need and finding a proof for it. Let's continue with the example question “When did Marcus die?” In order to
be able to answer this question, it must first be true that Marcus died. Thus it must be the case that
∃t: died(Marcus, t)
A reasonable first step then might be to try to prove this. To do so using resolution, we attempt to
show that
¬ ∃t: died(Marcus, i)
produces a contradiction. What does it mean for that statement to produce a contradiction?
Either it conflicts with a statement of the form
∀t: died(Marcus, t)
where t is a variable, in which ease we can either answer the question by reporting that there are
many times at which Marcus died, or we can simply pick one such time and respond with it. The
other possibility is that we produce a contradiction with one or more specific statements of the
form
died(Marcus, date)
for some specific value of date. Whatever value of date we use in producing that contradiction is
the answer we want. The value that proves that there is a value (and thus the inconsistency of
the statement that there is no such value) is exactly the value we want.
Figure 5. 14(a) shows how the resolution process finds the statement for which we are
looking. The answer to the question can then be derived from the chain of unifications that lead
back to the starting clause. We can eliminate the necessity for this final step by adding an
additional expression to the one we are going to use to try to find a contradiction.
This new expression will simply be the one we are trying to prove true (i.e., it will be the negation of the
expression that is actually used in the resolution). We can tag it with a special marker so that it will not
interfere with the resolution process. (In the figure, it is underlined.) It will just get carried along, but
each time unification is done, the variables in this dummy expression will be bound just as are the ones
in the clauses that are actively being used. Instead of terminating on reaching the nil clause, the
resolution procedure will terminate when all that is left is the dummy expression. The bindings of its
variables at that point provide the answer to the question. Figure 5.14(b) shows how this process
produces an answer to our question.
Forward and Backward Chaining
 Forward Chaining
• Forward chaining is a data driven method of deriving a
particular goal from a given knowledge base and set of
inference rules

• Inference rules are applied by matching facts to the

antecedents of consequence relations in the knowledge base

• The application of inference rules results in new knowledge

(from the consequents of the relations matched), which is
then added to the knowledge base

CPSC 433 Artificial Intelligence

 Forward Chaining
• Inference rules are successively applied to
elements of the knowledge base until the goal
is reached

• A search control method is needed to select

which element(s) of the knowledge base to
apply the inference rule to at any point in the
deduction

CPSC 433 Artificial Intelligence

 Forward Chaining Example
• Knowledge Base:
– If [X croaks and eats flies] Then [X is a frog]
– If [X chirps and sings] Then [X is a canary]
– If [X is a frog] Then [X is colored green]
– If [X is a canary] Then [X is colored yellow]
– [Fritz croaks and eats flies]
• Goal:
– [Fritz is colored Y]?

CPSC 433 Artificial Intelligence

Forward Chaining Example
Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog]
Then [X is colored green]

If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

Goal
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

Forward Chaining Example
Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog]
Then [X is colored green]

If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

Goal
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Forward Chaining Example
If [X croaks and eats flies] Knowledge Base
[Fritz croaks and eats flies] If [X croaks and eats flies]
Then [X is a frog] Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog]
[Fritz is a frog] Then [X is colored green]

If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

Goal
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Forward Chaining Example
If [X croaks and eats flies] Knowledge Base
[Fritz croaks and eats flies] If [X croaks and eats flies]
Then [X is a frog] Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog]
[Fritz is a frog] Then [X is colored green]

If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

[Fritz is a frog]

Goal
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Forward Chaining Example
If [X croaks and eats flies] Knowledge Base
[Fritz croaks and eats flies] If [X croaks and eats flies]
Then [X is a frog] Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog]
[Fritz is a frog] Then [X is colored green]

If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

[Fritz is a frog]

Goal
? [Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Forward Chaining Example
If [X croaks and eats flies] Knowledge Base
[Fritz croaks and eats flies] If [X croaks and eats flies]
Then [X is a frog] Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog]
[Fritz is a frog] Then [X is colored green]

If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

[Fritz is a frog]

Goal
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Forward Chaining Example
If [X croaks and eats flies] Knowledge Base
[Fritz croaks and eats flies] If [X croaks and eats flies]
Then [X is a frog] Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog] If [X is a frog]
[Fritz is a frog] Then [X is colored green]
Then [X is colored green]
If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

[Fritz is colored green] [Fritz is a frog]

Goal
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Forward Chaining Example
If [X croaks and eats flies] Knowledge Base
[Fritz croaks and eats flies] If [X croaks and eats flies]
Then [X is a frog] Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog] If [X is a frog]
[Fritz is a frog] Then [X is colored green]
Then [X is colored green]
If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

[Fritz is colored green] [Fritz is a frog]

[Fritz is colored green]

Goal
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Forward Chaining Example
If [X croaks and eats flies] Knowledge Base
[Fritz croaks and eats flies] If [X croaks and eats flies]
Then [X is a frog] Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog] If [X is a frog]
[Fritz is a frog] Then [X is colored green]
Then [X is colored green]
If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

[Fritz is colored green] [Fritz is a frog]

[Fritz is colored green]

Goal
? [Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Forward Chaining Example
If [X croaks and eats flies] Knowledge Base
[Fritz croaks and eats flies] If [X croaks and eats flies]
Then [X is a frog] Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog] If [X is a frog]
[Fritz is a frog] Then [X is colored green]
Then [X is colored green]
If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

[Fritz is colored green] [Fritz is a frog]

[Fritz is colored green]

Goal
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Forward Chaining Example
If [X croaks and eats flies] Knowledge Base
[Fritz croaks and eats flies] If [X croaks and eats flies]
Then [X is a frog] Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog] If [X is a frog]
[Fritz is a frog] Then [X is colored green]
Then [X is colored green]
If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

[Fritz is colored green] [Fritz is colored Y] ? [Fritz is a frog]

[Fritz is colored green]

Goal
Y = green [Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Backward Chaining
• Backward chaining is a goal driven method of deriving a
particular goal from a given knowledge base and set of
inference rules

• Inference rules are applied by matching the goal of the search

to the consequents of the relations stored in the knowledge
base

• When such a relation is found, the antecedent of the relation

is added to the list of goals (and not into the knowledge base,
as is done in forward chaining)

CPSC 433 Artificial Intelligence

 Backward Chaining
• Search proceeds in this manner until a goal
can be matched against a fact in the
knowledge base
– Remember: facts are simply consequence
relations with empty antecedents, so this is like
adding the ‘empty goal’ to the list of goals

• As with forward chaining, a search control

method is needed to select which goals will be
matched against which consequence relations
from the knowledge base
CPSC 433 Artificial Intelligence
Backward Chaining Example
Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog]
Then [X is colored green]

If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

Goals
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

Backward Chaining Example
Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X chirps and sings]

Then [X is a canary]

If [X is a frog]
Then [X is colored green]

If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

Goals
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X chirps and sings]

Then [X is colored green] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

Goals
[Fritz is colored Y]?

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X chirps and sings]

Then [X is colored green] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

Goals
[Fritz is colored Y]?

[X is a frog]

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X chirps and sings]

Then [X is colored green] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] If [X is a canary]
Then [X is colored yellow]

[Fritz croaks and eats flies]

Goals
[Fritz is colored Y]?

[X is a frog]

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X is a canary] If [X chirps and sings]

Then [X is colored green] Then [X is colored yellow] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] [X is a canary] If [X is a canary]

Then [X is colored yellow]

[Fritz croaks and eats flies]

Goals
[Fritz is colored Y]?

[X is a frog]

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X is a canary] If [X chirps and sings]

Then [X is colored green] Then [X is colored yellow] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] [X is a canary] If [X is a canary]

Then [X is colored yellow]

[Fritz croaks and eats flies]

Goals
[Fritz is colored Y]?

[X is a frog]

[X is a canary]

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X is a canary] If [X chirps and sings]

Then [X is colored green] Then [X is colored yellow] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] [X is a canary] If [X is a canary]

Then [X is colored yellow]

[Fritz croaks and eats flies]

Goals
[Fritz is colored Y]?

[X is a frog]

[X is a canary]

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X is a canary] If [X chirps and sings]

Then [X is colored green] Then [X is colored yellow] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] [X is a canary] If [X is a canary]

Then [X is colored yellow]

[Fritz croaks and eats flies]

If [X croaks and eats flies]
Then [X is a frog] Goals
[Fritz is colored Y]?

[X croaks and eats flies] [X is a frog]

[X is a canary]

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X is a canary] If [X chirps and sings]

Then [X is colored green] Then [X is colored yellow] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] [X is a canary] If [X is a canary]

Then [X is colored yellow]

[Fritz croaks and eats flies]

If [X croaks and eats flies]
Then [X is a frog] Goals
[Fritz is colored Y]?

[X croaks and eats flies] [X is a frog]

[X is a canary]

[X croaks and eats flies]

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X is a canary] If [X chirps and sings]

Then [X is colored green] Then [X is colored yellow] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] [X is a canary] If [X is a canary]

Then [X is colored yellow]

[Fritz croaks and eats flies]

If [X croaks and eats flies]
Then [X is a frog] Goals
[Fritz is colored Y]?

[X croaks and eats flies] [X is a frog]

[X is a canary]

[X croaks and eats flies]

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X is a canary] If [X chirps and sings]

Then [X is colored green] Then [X is colored yellow] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] [X is a canary] If [X is a canary]

Then [X is colored yellow]

[Fritz croaks and eats flies]

If [X croaks and eats flies]
Then [X is a frog] Goals
[Fritz is colored Y]?

[X croaks and eats flies] [Fritz croaks and eats flies] [X is a frog]

[X is a canary]

X = Fritz, Y = green [X croaks and eats flies]

CPSC 433 Artificial Intelligence

 Backward Chaining Example
[Fritz is colored Y] Knowledge Base
If [X croaks and eats flies]
Then [X is a frog]

If [X is a frog] If [X is a canary] If [X chirps and sings]

Then [X is colored green] Then [X is colored yellow] Then [X is a canary]

If [X is a frog]
Then [X is colored green]

[X is a frog] [X is a canary] If [X is a canary]

Then [X is colored yellow]

[Fritz croaks and eats flies]

If [X croaks and eats flies]
Then [X is a frog] Goals
[Fritz is colored Y]?

[X croaks and eats flies] [Fritz croaks and eats flies] [X is a frog]

[X is a canary]

X = Fritz, Y = green [X croaks and eats flies]

CPSC 433 Artificial Intelligence