Resolution

Inference in Logic:
• First-order predicate calculus has inference rules

• Inference rules: ways of deriving or proving new

statements from a given set of statements

Example: from the statements ab and bc,

one can derive the statement ac, written formally
as:
Inference and Logic Programming
• Inference Mechanism of logic programming
systems will be complex if is made to handle all of
first-order predicate calculus

Too many ways of expressing the same statements

Too many inference rules

• Most logic programming systems restrict

themselves to a particular subset of predicate
calculus called Horn clauses
Horn Clauses
Procedural interpretation: Horn clauses can be
viewed as procedures

 Here b can be assumed as a procedure, wherein the

body is the operations indicated by the ai’s

Horn clauses can also be viewed as specifications of

procedures rather than strictly as implementations

Example: specification of a sort procedure:

Horn Clauses (cont…)
• Horn clauses do not supply the algorithms, only the
properties that the result must have

• Most logic programming systems write Horn clauses

backward and drop the and connectives:

• Similarity to standard programming language

expression for the gcd:
Horn Clauses (Cont…)
• Variables:
Variables used in the head can be viewed as parameters
Variables used only in the body can be viewed as local,
temporary variables
• The scope of a variable is the clause in which it
appears
 Variables whose first appearance is on the left hand
side of the clause have implicit universal quantifiers
 Variables whose first appearance is in the body of the
clause have implicit existential quantifiers
Example:
grandmother(A, C) :- mother(A, B), mother(B, C).

for all A, C - A is the grandmother of C

if there exists a B such that A is the mother of B
and
B is the mother of C.

Another rule required is :

grandmother(A, C) :- mother(A, B), father(B, C).

Resolution and Unification
• Resolution: an inference rule for Horn clauses
If the head of the first Horn clause matches with one of
the statements in the body of the second Horn clause,
can replace the head with the body of the first in the
body of the second
Example: given two Horn clauses

If bi matches a, then we can infer this clause:

Resolution and Unification (cont...)
• Example:
given ba and cb
Resolution says ca
• Another way: combine left-hand and right-hand
sides of both clauses, and cancel statements that
match on both sides
Example:
given ba and cb
Combine: b,c,a,b
Cancel the b on both sides: ca
Resolution and Unification (cont...)
• A logic processing system uses resolution and
unification to match a goal and replace it with the
body, creating a new list of goals, called subgoals

• If all goals are eventually eliminated, deriving the

empty Horn clause, then the original statement has
been proved

• To match statements with variables, set the variables

equal to terms to make the statements identical and
then cancel from both sides
This process is called unification
Variables used this way are said to be instantiated
Resolution and Unification (cont...)
• Example: gcd with resolution and unification

• Goal:

• Resolution fails with first clause (10 does not match

0), so use the second clause and unify:
Resolution and Unification (cont…)
• Example (cont...):
If zero(10) is false, then not zero(10) is true
Simplify 15 mod 10 to 5, and cancel gcd (15, 10, x) from
both sides, giving:

Use unification as before:

To get this subgoal:

This now matches the first rule, so setting x to 5 gives the

empty statement
Resolution and Unification (cont...)
• A logic programming system must have a fixed
algorithm that specifies:
Order in which to attempt to resolve a list of goals
Order in which clauses are used to resolve goals

• In some cases, order can have a significant effect on

the answers found

• Logic programming systems using Horn clauses and

resolution with prespecified orders require that the
programmer is aware of the way the system
produces answers
Unification
• Unification: process by which variables are
instantiated to match during resolution
Basic expression whose semantics is determined by
unification is equality
• Prolog’s unification algorithm:
Constant unifies only with itself
Uninstantiated variable unifies with anything and
becomes instantiated to that thing
Structured term (function applied to arguments) unifies
with another term only if the same function name and
same number of arguments
Unification (Cont...)
• Examples:
Unification (Cont...)
• Unification causes uninstantiated variables to share
memory (to become aliases of each other)
•
Example: two uninstantiated variables are unified
Resolution in Prolog
• To run a Prolog program, one asks the interpreter a
question
• This is done by stating a theorem - asserting a
predicate - which the interpreter tries to prove
 If it can, it says yes
 If it can't, it says no
 If the predicate contained variables, the
interpreter prints the values it had to give them to
make the predicate true.
Resolution in Prolog (Cont…)
• Prolog searches for a resolution sequence that
satisfies the goal
• In order to satisfy the logical predicate, we can
imagine two search strategies:
Forward chaining, derived the goal from the axioms
Backward chaining, start with the goal and attempt to
resolve them working backwards
• Backward chaining is usually more efficient, so it is
the mechanism underlying the execution of Prolog
programs
Forward chaining is more efficient when the number of
facts is small and the number of rules is very large
 Resolution in Prolog (Cont…)
• The predicate that is asked for is the interpreter's original
GOAL
 In an attempt to SATISFY that goal, it looks for facts or rules with
which the goal can be UNIFIED

 Unification is a process by which compatible statements

are merged

 If it finds a fact; it succeeds

 If it finds a rule, it attempts to satisfy the terms in the body of

the rule in depth first order
Resolution in Prolog (Cont…)
 This process is motivated by the RESOLUTION
PRINCIPLE, due to Robinson:

If bi matches a, then we can infer this clause:

 Any variables that do not yet have values but which

correspond to constants or to variables with values in
the other clause get INSTANTIATED with that value

 Anyplace where uninstantiated variables correspond,

those variables are identified with each other, but
remain without values
Prolog’s Search Strategy
• Prolog applies resolution in a strictly linear fashion
Replaces goals from left to right
Considers clauses in the database from top down
Subgoals are considered immediately
This search strategy results in a depth-first search on a
tree of possible choices
• Example:
Prolog’s Search Strategy (cont’d.)
Prolog’s Search Strategy (cont’d.)

• Leaf nodes in the tree occur either when no match is found for the
leftmost clause or when all clauses have been eliminated (success)
• If failure, or the user indicates a continued search with a semicolon,
Prolog backtracks up the tree to find further paths
• Depth-first strategy is efficient: can be implemented in a stack-based
or recursive fashion
• Can be problematic if the search tree has branches of infinite depth
Prolog
• When it attempts resolution, the Prolog interpreter
pushes the current goal onto a stack, makes the first
term in the body the current goal, and goes back to
the beginning of the database and starts looking
again
• If it gets through the first goal of a body successfully,
the interpreter continues
with the next one
• If it gets all the way through the body, the goal is
satisfied and it backs up a level and proceeds
 Prolog
• If it fails to satisfy the terms in the body of a rule, the
interpreter undoes the unification of the left hand side
(this includes uninstantiating any variables that were
given values as a result of the unification) and keeps
looking through the database for something else with
which to unify (This process is called BACKTRACKING)

• If the interpreter gets to the end of database without

succeeding, it backs out a level (that's how it might fail to
satisfy something in a body) and continues from there
 Backward Chaining in Prolog
• Backward chaining follows a classic depth-first backtracking algorithm
• Goal:
Snowy(C)