26 Resolution

Bhushan Trivedi

Introduction

We have seen how predicate logic is used for representing facts and rules and thus help in reasoning from the same. Backward chaining, the process that we have seen for reasoning, is not very efficient, many conversions are required and complex unification process with special treatment for universal and existential quantifiers is also required. Resolution is a much simpler process which can also be implemented in a software program quite easily. We will study the process to convert a predicate logic statements into a form suitable for resolution. We will also see how we can prove anything using resolution after that.

Conversion to Clausal form

Before embarking on resolution, we must know how to convert a predicate logic statement into a clausal form.

The clausal form is one without either universal or existential quantifier, everything is universally quantified, no implication, no and, and only or symbol between predicates. It is a very simplified expression based on a simple algorithm which we are discussing next. Let us take following statement for conversion to a clausal form.

∀??∃??Person(X) ⋀ House (H,X) ⋀ Lost (X,H,2000) → Relief (Government, X)

Step 1. Remove the → (implication) using a rule A → B is same as ¬ A ⋁ B

Let us apply this rule over the statement.

∀??∃??¬ ((Person(X) ⋀ House (H,X) ⋀ Lost (X,H,2000)) ⋁ Relief (Government, X)

Step 2. Now apply negation to each item in the bracket so we will have negation confined to

one term only. There are a few important results one can use for moving negation to the single item.

1. ¬ (¬Predicate) = Predicate

2. ¬ (Predicate1 ⋁ Predicate2) = ¬ Predicate1 ⋀¬Predicate2

3. ¬ (Predicate1 ⋀ Predicate2) = ¬ Predicate1 ⋁¬Predicate2

4. ¬ (∀??Predicate) = ∃x ¬Predicate

5. ¬ (∃x Predicate) = ∀??¬Predicate

Applying step 2 yields following. You can see that we are applying rule 3 of above. Any other

rule, if applicable, can be applied in this case.

∀??∃??¬ Person(X) ⋁¬House (H,X)⋁¬Lost (X,H,2000) ⋁ Relief (Government, X)

Step 3

Use different names of variables for different clauses. Though we have not done that in our case but one can actually write something like following.

∀??Predicate1(X)⋀∀??Predicate2 (X)

In above case, we have two variables being named as x but they mean different things. We will name them differently in this particular step. You can see that we have anyway avoided that in our representation. This step is required if the designer has not done so. Above statement will be converted to following.

∀??Predicate1(X)⋀∀??Predicate2 (Y)

We have already done so in our case so the statement remains the same as before

∀??∃??¬ Person(X) ⋁¬House (H,X) ⋁¬Lost (X,H,2000) ⋁ Relief (Government, X)

Step 4.

Take all quantifiers on the left side of the statement. In our case we have already done so.

If the statement is ∀??Predicate1(X)⋁∀??Predicate2 (Y)

We will convert that to

∀??∀??Predicate1(X)⋁ Predicate2 (Y)

Anyway, our statement is not affected by application of this rule.

∀??∃??¬ Person(X) ⋁¬House (H,X) ⋁¬Lost (X,H,2000) ⋁ Relief (Government, X)

Step 5

Eliminate all existential quantifiers. We have already seen how we can do it by replacing the predicate variable by a constant value. In above case we have ∃??which we need to  remove now. The process is to replace all occurrences of H by a constant value; let us use H1 like before. Once we do that, we can remove the existential quantifier.

∀??¬ Person(X) ⋁¬House (H1,X) ⋁¬Lost (X,H1,2000) ⋁ Relief (Government, X)

Sometimes the process is not as straight forward as this. For example if there are multiple houses and we are dealing with H values for more than one person, we cannot simply state H1. This value of house depends on the owner. For example we may have Ramji and Kisnaji whose houses are destroyed during the earthquake. We will have to somehow relate house values that we derive dependent on the value of the person we are dealing with. The value of X in person (X) determines the house. That means all occurrences of H is to be replaced by a function which takes the argument as X and returns house that X owns. That means if we define that function Houseof(X) which returns the house of X. Thus we will have to replace H by Houseof(X). Such a function is known as Skolem Function. Thus our statement now reads as follows.

∀??¬ Person(X) ⋁¬House (Houseof (X) ,X) ⋁¬Lost (X,Houseof (X) ,2000) ⋁ Relief (Government,

X)1

Step 6.

Now we can drop all universal quantifiers. We have only one so we will be doing that easily

¬ Person(X) ⋁¬House (Houseof (X) ,X) ⋁¬Lost (X,Houseof (X) ,2000) ⋁ Relief (Government, X)

“1 Though we do not really need Skolem function here, a constant would do but we are doing it to demonstrate the use.”

You can see that the resultant value is in the clausal form now. In some cases it is not. To convert them into clausal form three more rules are needed which are discussed next. Step 7 We need to have all clauses (Components of the statements) in a form of (Part 1) and (Part 2) and (Part 3) … For that we might encounter two cases where one is a subset of another. Let us take both cases one after another.

1. Predicate1 ⋁ (Predicate 2 ⋀ Predicate 3)

= (Predicate 1 ⋁ Predicate 4) ⋀ (Predicate 1 ⋁ Predicate 3)

2. (Predicate1 ⋀ predicate 4) ⋁ (Predicate 2 ⋀ Predicate 3)

= (Predicate 1 ⋁ Predicate 2) ⋀

(Predicate 1 ⋁ Predicate 3) ⋀

(Predicate 4 ⋁ Predicate 2) ⋀

(Predicate 4 ⋁ Predicate 3)

Thus if we have

Player(Anand, Chess) ⋁ (Player (Jay, Badminton)⋀ Player(Jay,Chess)) we will have to convert it to

(Player(Anand, Chess) ⋁ Player (Jay, Badminton))⋀ (Player(Anand, Chess) ⋁ Player(Jay,Chess))

And if we have

(Player(Anand, Chess) ⋀ Player (Sanya, Tennis)) ⋁ ((Player (Jay, Badminton)⋀ Player(Jay,Chess)),

it will be converted to

(Player(Anand, Chess) ⋁ Player (Jay, Badminton))⋀ (Player(Anand, Chess) ⋁ Player(Jay,Chess)) ⋀ (Player (Sanya, Tennis) ⋁ Player (Jay, Badminton))⋀ (Player (Sanya, Tennis)⋁ Player(Jay,Chess))

Step 8

In this step, if the statement contains multiple clauses connected by ⋀ they will be treated as

separate clauses. Thus above example will be converted to

1. (Player(Anand, Chess) ⋁ Player (Jay, Badminton))

2. (Player(Anand, Chess) ⋁ Player(Jay,Chess))

3. (Player (Sanya, Tennis) ⋁ Player (Jay, Badminton))

4. (Player (Sanya, Tennis) ⋁ Player(Jay,Chess))

Step 9

If there is more than one variable quantified by a single universal quantifier, provide one for each such variable. For example

∀??(Player(X) ⋀ Winner(X)) must be converted to

∀??(Player(X) ⋀ ∀??Winner(X))

And now both of them are to be treated as separate clauses. That means

1.  ∀??(Player(X)

2.  ∀??Winner(X)

The purpose of above transformation is to make sure variables are not bound unnecessarily and incorrectly. For example we get Player(Anand) we may use 1 without really binding Winner. A player may not be a winner and thus if we do not bind X in Winner(X) we are saved from that trouble.

The  statement  written  using  conventional  predicate  logic  format  is  sometimes  known  as  Well Formed

The process of resolution, is quite straight forward. It is about taking any two clauses from the set of clauses, called parent clauses, and generate an inferred clause.

For example if we have two clauses

1. Player(Jay,Badminton) ⋁ Player(Anand, Chess)

2. ¬Player (Jay, Badminton) ⋁ Player (Saina, Badminton)

Remember these two clauses are basically premises, things known to be true. Thus combining both of them also yields true. Also any predicate of type ¬ Predicate ⋁predicate will always be true. For example ¬Player (Jay, Badminton) ⋁ Player(Jay,Badminton) will always be true as Jay is either a badminton player or he is not. Such combinations of clauses which are already true are eliminated from the resolved clauses. And thus the resultant clause in above case is Player(Anand, Chess) ⋁ Player (Saina, Badminton) In other words, during resolution, if there are two literals with same value and opposite sign, they are eliminated from the resultant clause.

This process becomes little complicated when the variables are used. For example if we have two clauses

Man (Ramji)

¬Man(X) ⋁Person (X)

We cannot resolve these two clauses unless both of them are unified. We have looked at the process of unification in the previous module. If we can unify X with Ramji, we get complementary literals i.e. Man (Ramji) and ¬Man(Ramji). What is the resultant clause? It is not Person(X) but Person (Ramji) as all instances of X will be bound with same value.

Producing a proof

Whenever we need to prove something, we need to negate that and add to the list of clauses. This addition must prove contradiction if what we want to prove is actually true.

For example if we want to prove Relief (Government, Ramji), what we will do is to add another

statement to the list of clauses

¬Relief (Government, Ramji)

Once we do that, we can start the process of resolution. The idea is to get a null statement at the end of the process. What we have taken is a contradiction to the truth and thus when we resolve the untrue statement (or clause) with true clauses, it should eventually cancel out each other and we must get a null statement. We will soon do so but there are a few important guidelines we must look at before we start working on it.

1. As long as possible, we will involve one clause that is resulted from the newly added clause for proving. As this clause is likely to be false, it is easier for us to get to the result. On the contrary, if we resolve clauses which does not involve this clause and we can find a null statement, that means original set of clauses had one false clause which is quite unlikely and thus there is no point doing that.

2. As long as possible, we need to find a literal which is complementary to one that we have in our expression for the other clause that we want to resolve. For example if we have a clause ¬BuildHouse(H) ⋁Lost(X,H,2000) as one of the clause, and if we have one more clause in the premise  as  BuildHouse(H) as  one part,  it  is  highly recommended  to  use  that  clause  as another parent. It is because ¬BuildHouse and BuildHouse will cancel each other out in the resolvent.

3. Choose  other  parent  clause  which  is  as  short  as  possible.  This  will  reduce  the  size  of resultant clause and improves the chances of getting to a null clause.

Too much of theory. Now it is the time for the experiment! Let us take one example that we have seen in the previous module and convert that in the clausal form for proof.

Proving using resolutionLet us pick up example 25.1

1. Man (Ramji)

2. Farmer (Ramji)

3. ∀??Kuchchhi(X) → Gujrati (X)

4. Belongsto (Ramji, Bhachau)

5. ∀??∃??Person(X) ⋀Belongsto (X,Bhachau) ⋀ House (H,X) → Lost (X,H,2000)

6. ∀??∃??Person(X) ⋀ House (H,X) ⋀ Lost (X,H,2000) → Relief (Government, X)

7.  ∀??Man(X) → Person(X)

8. ∃??House (H,Ramji)

Converting them to a clausal form yields following.

1. Man(Ramji)

2. Farmer(Ramji)

3. ¬Kuchchhi(X) ⋁Gujrati (X)

4. Belongto (Ramji, Bhachau)

5. ¬Person(X) ⋁¬Belongsto (X,Bhachau) ⋁¬House (Houseof(X),X) ⋁ Lost (X,Hosueof(X),2000)

6. ¬Person(X) ⋁¬House (Houseof(X),X) ⋁¬Lost (X,Houseof(X),2000) ⋁Relief (Government, X)

7. ¬ Man(X) ⋁ Person(X)

8. House(Houseof(Ramji), Ramji)

Now let us pick up what we want to prove. Ramji received a relief from the government.

9. ¬Relief (Government, Ramji)

Figure 26.1 The resolution process

The complete resolution process is depicted in the figure 26.1.

Another thing to notice is that we have to deal with similar resolution (House and ¬ House, Man and ¬Man etc). Even though the resolution process is quite simple and straightforward compared to backward chaining. It is easier to program as well. The only issue about this process is that it is hard to explain the proceedings.

Let us take another example to reiterate.

1. Man(Ramji)

2. Farmer(Ramji)

3. Belongto (Ramji, Bhachau)

4. ∀??∃??Person(X) ⋀Belongsto (X, Bhachau) ⋀ House (H,X) → Lost (X,H,2000)

5. ∀??∀??∃??Person(X) ⋀ House (H,X) ⋀ Lost (X,H,2000) → Relief (Government, X)

6. ∃??BuildHouse (H, Ramji, 2003)⋀ ¬ Changedhouse(Ramji,H,2015)

7.  ∀??∀??1∀??2∀??3∃??Buildhouse(H,X,T1)⋀¬ Changedhouse(X,H,T2)   ⋀   Between(T3,T1,T2)

→Liveinhouse(H,X,T3)

Now we need to prove that Ramji lived in his house in 2010. So we take a negation and provide it as 8th clause.

8. ¬Liveinhouse(H,Ramji,2010)

Now, let us convert these statements into clausal forms.

1. Man(Ramji)

2. Farmer(Ramji)

3. Belongto (Ramji, Bhachau)

4. ¬Person(X) ⋁¬Belongsto (X,Bhachau) ⋁¬House (Houseof(X),X) ⋁ Lost (X,Hosueof(X),2000)

5. ¬Person(X) ⋁¬House (,X) ⋁¬Lost (X,Houseof(X),2000) ⋁Relief (Government, X)

6. BuildHouse (Houseof(Ramji), Ramji, 2003)

7. ¬ Changedhouse(Ramji, Houseof(Ramji),2015)

8. ¬ Buildhouse(Houseof(Ramji),Ramji,T1)⋁Changedhouse(Ramji, Houseof(Ramji),T2)

⋁¬ Between(T3,T1,T2) ⋁Liveinhouse(Houseof(Ramji),Ramji,T3)

9. ¬Liveinhouse(Houseof(Ramji),Ramji,2010)

Note that statement no. 6 is divided into  two clauses connected by and thus the step

number 8 is applied.

The resolution process is depicted in figure 26.2.

We can see that the resolution process is able to prove things using refutation (negation) and it works using a simple mechanism. The issues that we have discussed in the previous module like using the process for answering questions, need for unification and consistently assigning values to variables, need to try multiple values if the answer is not sought from first and so are equally valid for the resolution process as well.

The predicate logic seems to be a very good method for storing and inferring from knowledge. However, there are some issues with this basic form of knowledge representation. We will soon see what the problem with this approach is and how we can improve using other methods in the next two module.

Figure 26.2 The resolution process for predicates with function

Summary

The resolution is a simpler process than backward chaining but demands simpler representation of the statements as disjunction of literals. The disjunction of literals is known as clausal form. Conversion to the clausal form is done using a simple algorithm. It starts from removing implication, making necessary changes to drop universal and existential quantifiers, convert and separate clauses connected by ⋀ and then write them as separate rules. The last step is to standardize the variables apart. Once all these steps are applied, all wffs are converted to clausal form. Once converted to clausal form, we can add negation of the statement which we want to prove again in clausal form and use resolution to generate contradiction in form of a null statement. We have used the resolution process on two examples we have seen in the previous chapter.