Resolution yields a complete inference algorithm when coupled with any complete
search algorithm.Resolution makes use of the inference rules. Resolution
performs deductive inference.Resolution uses proof by contradiction. One can
perform Resolution from a Knowledge Base. A Knowledge Base is a collection of facts
or one can even call it a database with all facts.

**Resolution Algorithm:**

Resolution basically works
by using the principle of proof by contradiction. To find the conclusion we
should negate the conclusion. Then the resolution rule is applied to the resulting
clauses. Each clause that contains complementary literals is resolved to
produce a two new clause,which can be added to the set of facts (if it is not
already present).This process continues until one of the two things happen:

·
There are no new clauses that can be added

·
An application of the resolution rule derives the empty clause

An empty clause shows that the negation of the conclusion is a complete
contradiction ,hence the negation of the conclusion is invalid or false or the
assertion is completely valid or true.

Steps for Resolution Refutation

1 1. Convert all the propositions of KB to clause form (S).

2. Negate a and convert it to clause form. Add it to S.

3. Repeat until either a contradiction is found or no progress can

be made:

2. Negate a and convert it to clause form. Add it to S.

3. Repeat until either a contradiction is found or no progress can

be made:

**Unification:**

In propositional logic it is
easy to determine that two literals can not both be true at the same
time. Simply look for L and ~L . In predicate logic, this matching
process is more complicated, since bindings of variables must be
considered.

For example man
(john) and man(john) is a contradiction while man (john) and
man(Himalayas) is not. Thus in order to determine contradictions we need
a matching procedure that compares two literals and discovers whether
there exist a set of substitutions that makes them identical . There is a
recursive procedure that does this matching . It is called Unification
algorithm.

In
Unification algorithm each literal is represented as a list, where
first element is the name of a predicate and the remaining elements are
arguments. The argument may be a single element (atom) or may be another
list. For example we can have literals as

The Unification algorithm is
listed below as a procedure UNIFY (L1, L2). It returns a list
representing the composition of the substitutions that were performed
during the match. An empty list NIL indicates that a match was found
without any substitutions. If the list contains a single value F, it
indicates that the unification procedure failed.

**
**

**UNIFY (L1, L2)**

**
**

**1. if L1 or L2 is an atom part of same thing do**

**
**

**(a) if L1 or L2 are identical then return NIL**

**
**

**(b) else if L1 is a variable then do**

**
**

**(i) if L1 occurs in L2 then return F else return (L2/L1)**

**
**

**else if L2 is a variable then do**

**
**

**(i) if L2 occurs in L1 then return F else return (L1/L2)**

**
**

**else return F.**

**
**

**2. If length (L!) is not equal to length (L2) then return F.**

**
**

**3. Set SUBST to NIL**

**
**

**( at the end of this procedure , SUBST will contain all the substitutions used to unify L1 and L2).**

**
**

**4. For I = 1 to number of elements in L1 do**

**
**

**i) call UNIFY with the i th element of L1 and I’th element of L2, putting the result in S**

**
**

**ii) if S = F then return F**

**
**

**iii) if S is not equal to NIL then do**

**
**

**(A) apply S to the remainder of both L1 and L2**

**
**

**(B) SUBST := APPEND (S, SUBST) return SUBST.**

**Resolution in Prepositional Logic**

We start by converting this first sentence into conjunctive normal fom.
We don’t actually have to do anything. It’s already in the right form. Now, “P
implies R” turns into “not P or R”. Similarly,
“Q implies R” turns into “not Q or R .

We start by converting this first sentence into conjunctive normal fom.
We don’t actually have to do anything. It’s already in the right form. Now, “P
implies R” turns into “not P or R”. Similarly,
“Q implies R” turns into “not Q or R .

Now we want to add one more thing to our list of given statements. What's
it going to be? Not R. Right?We're gong to assert the negation of the thing we're trying to prove. We'd like to prove that R follows from these
things. But what we're going to do instead is say not R, and now we're trying
to prove false. And if we manage to prove false, then we will have a proof that
R is entailed by the assumptions.

And now, we look for opportunities to apply
the resolution rule. You can do it in any order you like (though some orders of
application will result in much shorter proofs than others). We can apply
resolution to lines 1 and 2, and get “Q or R” by resolving away P. And we can
take lines 2 and 4, resolve away R, and get “not P.” Similarly, we can take lines
3 and 4, resolve away R, and get “not Q”. By
resolving away Q in lines 5 and 7, we get R. And finally, resolving away R in lines 4 and 8, we get the empty clause,
which is false. We’ll often draw this little black box to indicate that we’ve
reached the desired contradiction.

**Resolution in Predicate Logic**

Consider the example,

**“All Romans who know Marcus either hate Caesar or think that anyone who hates anyone is crazy”**

**Step 1:**Convert the given statements in Predicate/Propositional Logic

**Consider the following example,**

**Example1:**

**Clause Form:**