{"id":217,"date":"2018-07-13T09:56:20","date_gmt":"2018-07-13T09:56:20","guid":{"rendered":"http:\/\/itp6.epgpbooks.inflibnet.ac.in\/?post_type=chapter&p=217"},"modified":"2019-05-16T05:29:17","modified_gmt":"2019-05-16T05:29:17","slug":"resolution","status":"publish","type":"chapter","link":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/chapter\/resolution\/","title":{"rendered":"Resolution"},"content":{"raw":"
\"epgp<\/a>\r\n<\/span><\/div>\r\n
\r\n\r\n \r\n

Introduction<\/strong><\/p>\r\n \r\n

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.<\/p>\r\n \r\n

Conversion to Clausal form<\/strong><\/p>\r\n \r\n

Before embarking on resolution, we must know how to convert a predicate logic statement into a clausal form.<\/p>\r\n \r\n

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.<\/p>\r\n \r\n

\u2200??\u2203??Person(X) \u22c0 House (H,X) \u22c0 Lost (X,H,2000) \u2192 Relief (Government, X)<\/p>\r\n

Step 1. Remove the \u2192 (implication) using a rule A \u2192 B is same as \u00ac A \u22c1 B<\/p>\r\n

Let us apply this rule over the statement.<\/p>\r\n

\u2200??\u2203??\u00ac ((Person(X) \u22c0 House (H,X) \u22c0 Lost (X,H,2000)) \u22c1 Relief (Government, X)<\/p>\r\n \r\n

Step 2. Now apply negation to each item in the bracket so we will have negation confined to<\/p>\r\n

one term only. There are a few important results one can use for moving negation to the single item.<\/p>\r\n \r\n

1. \u00ac (\u00acPredicate) = Predicate<\/p>\r\n

2. \u00ac (Predicate1 \u22c1 Predicate2) = \u00ac Predicate1 \u22c0\u00acPredicate2<\/p>\r\n

3. \u00ac (Predicate1 \u22c0 Predicate2) = \u00ac Predicate1 \u22c1\u00acPredicate2<\/p>\r\n

4. \u00ac (\u2200??Predicate) = \u2203x \u00acPredicate<\/p>\r\n

5. \u00ac (\u2203x Predicate) = \u2200??\u00acPredicate<\/p>\r\n \r\n

Applying step 2 yields following. You can see that we are applying rule 3 of above. Any other<\/p>\r\n

rule, if applicable, can be applied in this case.<\/p>\r\n \r\n

\u2200??\u2203??\u00ac Person(X) \u22c1\u00acHouse (H,X)\u22c1\u00acLost (X,H,2000) \u22c1 Relief (Government, X)<\/p>\r\n \r\n

Step 3<\/p>\r\n

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.<\/p>\r\n \r\n

\u2200??Predicate1(X)\u22c0\u2200??Predicate2 (X)<\/p>\r\n\r\n<\/div>\r\n \r\n

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.<\/span><\/p>\r\n\r\n

\r\n\r\n \r\n\r\n\u2200??Predicate1(X)\u22c0\u2200??Predicate2 (Y)\r\n\r\n \r\n\r\nWe have already done so in our case so the statement remains the same as before\r\n\r\n\u2200??\u2203??\u00ac Person(X) \u22c1\u00acHouse (H,X) \u22c1\u00acLost (X,H,2000) \u22c1 Relief (Government, X)\r\n\r\n \r\n\r\nStep 4.\r\n\r\n \r\n\r\nTake all quantifiers on the left side of the statement. In our case we have already done so.\r\n\r\nIf the statement is \u2200??Predicate1(X)\u22c1\u2200??Predicate2 (Y)\r\n\r\nWe will convert that to\r\n\r\n\u2200??\u2200??Predicate1(X)\u22c1 Predicate2 (Y)\r\n\r\nAnyway, our statement is not affected by application of this rule.\r\n\r\n\u2200??\u2203??\u00ac Person(X) \u22c1\u00acHouse (H,X) \u22c1\u00acLost (X,H,2000) \u22c1 Relief (Government, X)\r\n\r\n \r\n\r\nStep 5\r\n\r\n \r\n

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 \u2203??which we need to \u00a0remove\u00a0now. The process is to replace all occurrences of H by a constant value; let us use H1 like before.\u00a0Once we do that, we can remove the existential quantifier.<\/p>\r\n \r\n\r\n\u2200??\u00ac Person(X) \u22c1\u00acHouse (H1,X) \u22c1\u00acLost (X,H1,2000) \u22c1 Relief (Government, X)\r\n\r\n \r\n

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.<\/p>\r\n \r\n\r\n\u2200??\u00ac Person(X) \u22c1\u00acHouse (Houseof (X) ,X) \u22c1\u00acLost (X,Houseof (X) ,2000) \u22c1 Relief (Government,\r\n\r\nX)1<\/a>\r\n\r\n \r\n\r\nStep 6.\r\n\r\n \r\n\r\nNow we can drop all universal quantifiers. We have only one so we will be doing that easily\r\n\r\n\u00ac Person(X) \u22c1\u00acHouse (Houseof (X) ,X) \u22c1\u00acLost (X,Houseof (X) ,2000) \u22c1 Relief (Government, X)\r\n\r\n \r\n

\"1 Though we do not really need Skolem function here, a constant would do but we are doing it to demonstrate the use.\"<\/em><\/p>\r\n\r\n<\/div>\r\n \r\n

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

\r\n\r\n \r\n\r\n1. Predicate1 \u22c1 (Predicate 2 \u22c0 Predicate 3)\r\n\r\n= (Predicate 1 \u22c1 Predicate 4) \u22c0 (Predicate 1 \u22c1 Predicate 3)\r\n\r\n2. (Predicate1 \u22c0 predicate 4) \u22c1 (Predicate 2 \u22c0 Predicate 3)\r\n\r\n= (Predicate 1 \u22c1 Predicate 2) \u22c0\r\n\r\n(Predicate 1 \u22c1 Predicate 3) \u22c0\r\n\r\n(Predicate 4 \u22c1 Predicate 2) \u22c0\r\n\r\n(Predicate 4 \u22c1 Predicate 3)\r\n\r\n \r\n\r\nThus if we have\r\n\r\n \r\n\r\nPlayer(Anand, Chess) \u22c1 (Player (Jay, Badminton)\u22c0 Player(Jay,Chess)) we will have to convert it to\r\n\r\n(Player(Anand, Chess) \u22c1 Player (Jay, Badminton))\u22c0 (Player(Anand, Chess) \u22c1 Player(Jay,Chess))\r\n\r\nAnd if we have\r\n\r\n(Player(Anand, Chess) \u22c0 Player (Sanya, Tennis)) \u22c1 ((Player (Jay, Badminton)\u22c0 Player(Jay,Chess)),\r\n\r\nit will be converted to\r\n\r\n(Player(Anand, Chess) \u22c1 Player (Jay, Badminton))\u22c0 (Player(Anand, Chess) \u22c1 Player(Jay,Chess)) \u22c0 (Player (Sanya, Tennis) \u22c1 Player (Jay, Badminton))\u22c0 (Player (Sanya, Tennis)\u22c1 Player(Jay,Chess))\r\n\r\n \r\n\r\nStep 8\r\n\r\n \r\n\r\nIn this step, if the statement contains multiple clauses connected by \u22c0 they will be treated as\r\n\r\nseparate clauses. Thus above example will be converted to\r\n\r\n1. (Player(Anand, Chess) \u22c1 Player (Jay, Badminton))\r\n\r\n2. (Player(Anand, Chess) \u22c1 Player(Jay,Chess))\r\n\r\n3. (Player (Sanya, Tennis) \u22c1 Player (Jay, Badminton))\r\n\r\n4. (Player (Sanya, Tennis) \u22c1 Player(Jay,Chess))\r\n\r\n \r\n\r\nStep 9\r\n\r\n \r\n\r\nIf there is more than one variable quantified by a single universal quantifier, provide one for each such variable. For example\r\n\r\n\u2200??(Player(X) \u22c0 Winner(X)) must be converted to\r\n\r\n\u2200??(Player(X) \u22c0 \u2200??Winner(X))\r\n\r\n<\/div>\r\n
\r\n\r\n \r\n\r\nAnd now both of them are to be treated as separate clauses. That means\r\n\r\n \r\n\r\n1.\u00a0 \u2200??(Player(X)\r\n\r\n2.\u00a0 \u2200??Winner(X)\r\n\r\n \r\n

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\u00a0may not be a winner and thus if we do not bind X in Winner(X) we are saved from that trouble.<\/p>\r\n \r\n

The \u00a0statement \u00a0written \u00a0using \u00a0conventional \u00a0predicate \u00a0logic \u00a0format \u00a0is \u00a0sometimes \u00a0known \u00a0as \u00a0Well Formed<\/p>\r\n \r\n

The process of resolution, is quite straight forward. It is about taking any two clauses from the set of clauses, called pa<\/em>rent <\/em>clauses, and generate an inferred clause.<\/p>\r\n \r\n\r\nFor example if we have two clauses\r\n\r\n1. Player(Jay,Badminton) \u22c1 Player(Anand, Chess)\r\n\r\n2. \u00acPlayer (Jay, Badminton) \u22c1 Player (Saina, Badminton)\r\n\r\n \r\n

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 \u00ac Predicate \u22c1predicate will always be true. For example \u00acPlayer (Jay, Badminton) \u22c1 Player(Jay,Badminton) will always be true as Jay is either a\u00a0badminton player or he is not. Such combinations of clauses which are already true are eliminated\u00a0from the resolved clauses. And thus the resultant clause in above case is\u00a0Player(Anand, Chess) \u22c1 Player (Saina, Badminton)\u00a0In other words, during resolution, if there are two literals with same value and opposite sign, they\u00a0<\/em>a<\/em>r<\/em>e eliminated from the resultant clause.<\/em><\/p>\r\n \r\n\r\nThis process becomes little complicated when the variables are used. For example if we have two clauses\r\n\r\n \r\n\r\nMan (Ramji)\r\n\r\n\u00acMan(X) \u22c1Person (X)\r\n\r\n \r\n

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 \u00acMan(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.<\/p>\r\n \r\n

Producing a proof<\/strong><\/p>\r\n \r\n

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.<\/p>\r\n \r\n\r\nFor example if we want to prove Relief (Government, Ramji), what we will do is to add another\r\n\r\nstatement to the list of clauses\r\n\r\n\u00acRelief (Government, Ramji)\r\n\r\n \r\n

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\u00a0must 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.<\/span><\/p>\r\n\r\n<\/div>\r\n

\r\n\r\n \r\n

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.<\/p>\r\n \r\n

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\u00a0\u00acBuildHouse(H) \u22c1Lost(X,H,2000) as one of the clause, and if we have one more clause in the\u00a0premise \u00a0as \u00a0BuildHouse(H) as \u00a0one part, \u00a0it \u00a0is \u00a0highly recommended\u00a0 to \u00a0use \u00a0that \u00a0clause \u00a0as\u00a0another parent. It is because \u00acBuildHouse and BuildHouse will cancel each other out in the\u00a0resolvent.<\/p>\r\n \r\n

3. Choose \u00a0other \u00a0parent \u00a0clause \u00a0which \u00a0is \u00a0as \u00a0short \u00a0as \u00a0possible. \u00a0This \u00a0will \u00a0reduce \u00a0the \u00a0size \u00a0of resultant clause and improves the chances of getting to a null clause.<\/p>\r\n \r\n\r\nToo 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.\r\n\r\n \r\n\r\nProving using resolutionLet us pick up example 25.1\r\n\r\n \r\n\r\n1. Man (Ramji)\r\n\r\n2. Farmer (Ramji)\r\n\r\n3. \u2200??Kuchchhi(X) \u2192 Gujrati (X)\r\n\r\n4. Belongsto (Ramji, Bhachau)\r\n\r\n5. \u2200??\u2203??Person(X) \u22c0Belongsto (X,Bhachau) \u22c0 House (H,X) \u2192 Lost (X,H,2000)\r\n\r\n6. \u2200??\u2203??Person(X) \u22c0 House (H,X) \u22c0 Lost (X,H,2000) \u2192 Relief (Government, X)\r\n\r\n7.\u00a0 \u2200??Man(X) \u2192 Person(X)\r\n\r\n8. \u2203??House (H,Ramji)\r\n\r\n \r\n\r\nConverting them to a clausal form yields following.\r\n\r\n \r\n\r\n1. Man(Ramji)\r\n\r\n2. Farmer(Ramji)\r\n\r\n3. \u00acKuchchhi(X) \u22c1Gujrati (X)\r\n\r\n4. Belongto (Ramji, Bhachau)\r\n\r\n5. \u00acPerson(X) \u22c1\u00acBelongsto (X,Bhachau) \u22c1\u00acHouse (Houseof(X),X) \u22c1 Lost (X,Hosueof(X),2000)\r\n\r\n6. \u00acPerson(X) \u22c1\u00acHouse (Houseof(X),X) \u22c1\u00acLost (X,Houseof(X),2000) \u22c1Relief (Government, X)\r\n\r\n7. \u00ac Man(X) \u22c1 Person(X)\r\n\r\n8. House(Houseof(Ramji), Ramji)\r\n\r\n \r\n\r\nNow let us pick up what we want to prove. Ramji received a relief from the government.\r\n\r\n \r\n\r\n9. \u00acRelief (Government, Ramji)\r\n\r\n<\/div>\r\n

\r\n\r\n\"\"\r\n\r\n<\/div>\r\n
\r\n

F<\/em>i<\/em>gu<\/em>re 26.1 The resolution process<\/em><\/p>\r\n \r\n\r\nThe complete resolution process is depicted in the figure 26.1.\r\n\r\n<\/div>\r\n \r\n

Another thing to notice is that we have to deal with similar resolution (House and \u00ac House, Man and\u00a0<\/span>\u00acMan etc). Even though the resolution process is quite simple and straightforward compared to\u00a0<\/span>backward chaining. It is easier to program as well. The only issue about this process is that it is hard\u00a0<\/span>to explain the proceedings.<\/span><\/p>\r\n\r\n

\r\n\r\n \r\n\r\nLet us take another example to reiterate.\r\n\r\n \r\n\r\n1. Man(Ramji)\r\n\r\n2. Farmer(Ramji)\r\n\r\n3. Belongto (Ramji, Bhachau)\r\n\r\n4. \u2200??\u2203??Person(X) \u22c0Belongsto (X, Bhachau) \u22c0 House (H,X) \u2192 Lost (X,H,2000)\r\n\r\n5. \u2200??\u2200??\u2203??Person(X) \u22c0 House (H,X) \u22c0 Lost (X,H,2000) \u2192 Relief (Government, X)\r\n\r\n6. \u2203??BuildHouse (H, Ramji, 2003)\u22c0 \u00ac Changedhouse(Ramji,H,2015)\r\n\r\n7.\u00a0 \u2200??\u2200??1\u2200??2\u2200??3\u2203??Buildhouse(H,X,T1)\u22c0\u00ac Changedhouse(X,H,T2)\u00a0 \u00a0\u22c0\u00a0 \u00a0Between(T3,T1,T2)\r\n\r\n\u2192Liveinhouse(H,X,T3)\r\n\r\n \r\n

Now we need to prove that Ramji lived in his house in 2010. So we take a negation and provide it as 8th clause.<\/p>\r\n \r\n\r\n8. \u00acLiveinhouse(H,Ramji,2010)\r\n\r\n \r\n\r\nNow, let us convert these statements into clausal forms.\r\n\r\n \r\n\r\n1. Man(Ramji)\r\n\r\n2. Farmer(Ramji)\r\n\r\n3. Belongto (Ramji, Bhachau)\r\n\r\n4. \u00acPerson(X) \u22c1\u00acBelongsto (X,Bhachau) \u22c1\u00acHouse (Houseof(X),X) \u22c1 Lost (X,Hosueof(X),2000)\r\n\r\n5. \u00acPerson(X) \u22c1\u00acHouse (,X) \u22c1\u00acLost (X,Houseof(X),2000) \u22c1Relief (Government, X)\r\n\r\n6. BuildHouse (Houseof(Ramji), Ramji, 2003)\r\n\r\n7. \u00ac Changedhouse(Ramji, Houseof(Ramji),2015)\r\n\r\n8. \u00ac Buildhouse(Houseof(Ramji),Ramji,T1)\u22c1Changedhouse(Ramji, Houseof(Ramji),T2)\r\n\r\n\u22c1\u00ac Between(T3,T1,T2) \u22c1Liveinhouse(Houseof(Ramji),Ramji,T3)\r\n\r\n9. \u00acLiveinhouse(Houseof(Ramji),Ramji,2010)\r\n\r\n \r\n\r\nNote that statement no. 6 is divided into\u00a0 two clauses connected by and thus the step\r\n\r\nnumber 8 is applied.\r\n\r\n \r\n\r\nThe resolution process is depicted in figure 26.2.\r\n\r\n \r\n

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.<\/p>\r\n \r\n

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.<\/p>\r\n\r\n<\/div>\r\n

\"\"<\/p>\r\n

F<\/em>i<\/em>gu<\/em>re 26.2 The resolution process for predicates with function<\/em><\/p>\r\n \r\n

Summary<\/strong><\/p>\r\n \r\n

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 \u22c0 and then write them as separate rules. The last step is to standardize the variables\u00a0apart. Once all these steps are applied, all wffs are converted to clausal form. Once converted to\u00a0clausal 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.<\/p>\r\n\r\n\r\n\r\n
you can view video on Resolution<\/strong><\/td>\r\n\"\"<\/a><\/td>\r\n<\/tr>\r\n<\/tbody>\r\n<\/table>","rendered":"
\"epgp<\/a>
\n<\/span><\/div>\n
\n

 <\/p>\n

Introduction<\/strong><\/p>\n

 <\/p>\n

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.<\/p>\n

 <\/p>\n

Conversion to Clausal form<\/strong><\/p>\n

 <\/p>\n

Before embarking on resolution, we must know how to convert a predicate logic statement into a clausal form.<\/p>\n

 <\/p>\n

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.<\/p>\n

 <\/p>\n

\u2200??\u2203??Person(X) \u22c0 House (H,X) \u22c0 Lost (X,H,2000) \u2192 Relief (Government, X)<\/p>\n

Step 1. Remove the \u2192 (implication) using a rule A \u2192 B is same as \u00ac A \u22c1 B<\/p>\n

Let us apply this rule over the statement.<\/p>\n

\u2200??\u2203??\u00ac ((Person(X) \u22c0 House (H,X) \u22c0 Lost (X,H,2000)) \u22c1 Relief (Government, X)<\/p>\n

 <\/p>\n

Step 2. Now apply negation to each item in the bracket so we will have negation confined to<\/p>\n

one term only. There are a few important results one can use for moving negation to the single item.<\/p>\n

 <\/p>\n

1. \u00ac (\u00acPredicate) = Predicate<\/p>\n

2. \u00ac (Predicate1 \u22c1 Predicate2) = \u00ac Predicate1 \u22c0\u00acPredicate2<\/p>\n

3. \u00ac (Predicate1 \u22c0 Predicate2) = \u00ac Predicate1 \u22c1\u00acPredicate2<\/p>\n

4. \u00ac (\u2200??Predicate) = \u2203x \u00acPredicate<\/p>\n

5. \u00ac (\u2203x Predicate) = \u2200??\u00acPredicate<\/p>\n

 <\/p>\n

Applying step 2 yields following. You can see that we are applying rule 3 of above. Any other<\/p>\n

rule, if applicable, can be applied in this case.<\/p>\n

 <\/p>\n

\u2200??\u2203??\u00ac Person(X) \u22c1\u00acHouse (H,X)\u22c1\u00acLost (X,H,2000) \u22c1 Relief (Government, X)<\/p>\n

 <\/p>\n

Step 3<\/p>\n

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.<\/p>\n

 <\/p>\n

\u2200??Predicate1(X)\u22c0\u2200??Predicate2 (X)<\/p>\n<\/div>\n

 <\/p>\n

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.<\/span><\/p>\n

\n

 <\/p>\n

\u2200??Predicate1(X)\u22c0\u2200??Predicate2 (Y)<\/p>\n

 <\/p>\n

We have already done so in our case so the statement remains the same as before<\/p>\n

\u2200??\u2203??\u00ac Person(X) \u22c1\u00acHouse (H,X) \u22c1\u00acLost (X,H,2000) \u22c1 Relief (Government, X)<\/p>\n

 <\/p>\n

Step 4.<\/p>\n

 <\/p>\n

Take all quantifiers on the left side of the statement. In our case we have already done so.<\/p>\n

If the statement is \u2200??Predicate1(X)\u22c1\u2200??Predicate2 (Y)<\/p>\n

We will convert that to<\/p>\n

\u2200??\u2200??Predicate1(X)\u22c1 Predicate2 (Y)<\/p>\n

Anyway, our statement is not affected by application of this rule.<\/p>\n

\u2200??\u2203??\u00ac Person(X) \u22c1\u00acHouse (H,X) \u22c1\u00acLost (X,H,2000) \u22c1 Relief (Government, X)<\/p>\n

 <\/p>\n

Step 5<\/p>\n

 <\/p>\n

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 \u2203??which we need to \u00a0remove\u00a0now. The process is to replace all occurrences of H by a constant value; let us use H1 like before.\u00a0Once we do that, we can remove the existential quantifier.<\/p>\n

 <\/p>\n

\u2200??\u00ac Person(X) \u22c1\u00acHouse (H1,X) \u22c1\u00acLost (X,H1,2000) \u22c1 Relief (Government, X)<\/p>\n

 <\/p>\n

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.<\/p>\n

 <\/p>\n

\u2200??\u00ac Person(X) \u22c1\u00acHouse (Houseof (X) ,X) \u22c1\u00acLost (X,Houseof (X) ,2000) \u22c1 Relief (Government,<\/p>\n

X)1<\/a><\/p>\n

 <\/p>\n

Step 6.<\/p>\n

 <\/p>\n

Now we can drop all universal quantifiers. We have only one so we will be doing that easily<\/p>\n

\u00ac Person(X) \u22c1\u00acHouse (Houseof (X) ,X) \u22c1\u00acLost (X,Houseof (X) ,2000) \u22c1 Relief (Government, X)<\/p>\n

 <\/p>\n

“1 Though we do not really need Skolem function here, a constant would do but we are doing it to demonstrate the use.”<\/em><\/p>\n<\/div>\n

 <\/p>\n

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

\n

 <\/p>\n

1. Predicate1 \u22c1 (Predicate 2 \u22c0 Predicate 3)<\/p>\n

= (Predicate 1 \u22c1 Predicate 4) \u22c0 (Predicate 1 \u22c1 Predicate 3)<\/p>\n

2. (Predicate1 \u22c0 predicate 4) \u22c1 (Predicate 2 \u22c0 Predicate 3)<\/p>\n

= (Predicate 1 \u22c1 Predicate 2) \u22c0<\/p>\n

(Predicate 1 \u22c1 Predicate 3) \u22c0<\/p>\n

(Predicate 4 \u22c1 Predicate 2) \u22c0<\/p>\n

(Predicate 4 \u22c1 Predicate 3)<\/p>\n

 <\/p>\n

Thus if we have<\/p>\n

 <\/p>\n

Player(Anand, Chess) \u22c1 (Player (Jay, Badminton)\u22c0 Player(Jay,Chess)) we will have to convert it to<\/p>\n

(Player(Anand, Chess) \u22c1 Player (Jay, Badminton))\u22c0 (Player(Anand, Chess) \u22c1 Player(Jay,Chess))<\/p>\n

And if we have<\/p>\n

(Player(Anand, Chess) \u22c0 Player (Sanya, Tennis)) \u22c1 ((Player (Jay, Badminton)\u22c0 Player(Jay,Chess)),<\/p>\n

it will be converted to<\/p>\n

(Player(Anand, Chess) \u22c1 Player (Jay, Badminton))\u22c0 (Player(Anand, Chess) \u22c1 Player(Jay,Chess)) \u22c0 (Player (Sanya, Tennis) \u22c1 Player (Jay, Badminton))\u22c0 (Player (Sanya, Tennis)\u22c1 Player(Jay,Chess))<\/p>\n

 <\/p>\n

Step 8<\/p>\n

 <\/p>\n

In this step, if the statement contains multiple clauses connected by \u22c0 they will be treated as<\/p>\n

separate clauses. Thus above example will be converted to<\/p>\n

1. (Player(Anand, Chess) \u22c1 Player (Jay, Badminton))<\/p>\n

2. (Player(Anand, Chess) \u22c1 Player(Jay,Chess))<\/p>\n

3. (Player (Sanya, Tennis) \u22c1 Player (Jay, Badminton))<\/p>\n

4. (Player (Sanya, Tennis) \u22c1 Player(Jay,Chess))<\/p>\n

 <\/p>\n

Step 9<\/p>\n

 <\/p>\n

If there is more than one variable quantified by a single universal quantifier, provide one for each such variable. For example<\/p>\n

\u2200??(Player(X) \u22c0 Winner(X)) must be converted to<\/p>\n

\u2200??(Player(X) \u22c0 \u2200??Winner(X))<\/p>\n<\/div>\n

\n

 <\/p>\n

And now both of them are to be treated as separate clauses. That means<\/p>\n

 <\/p>\n

1.\u00a0 \u2200??(Player(X)<\/p>\n

2.\u00a0 \u2200??Winner(X)<\/p>\n

 <\/p>\n

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\u00a0may not be a winner and thus if we do not bind X in Winner(X) we are saved from that trouble.<\/p>\n

 <\/p>\n

The \u00a0statement \u00a0written \u00a0using \u00a0conventional \u00a0predicate \u00a0logic \u00a0format \u00a0is \u00a0sometimes \u00a0known \u00a0as \u00a0Well Formed<\/p>\n

 <\/p>\n

The process of resolution, is quite straight forward. It is about taking any two clauses from the set of clauses, called pa<\/em>rent <\/em>clauses, and generate an inferred clause.<\/p>\n

 <\/p>\n

For example if we have two clauses<\/p>\n

1. Player(Jay,Badminton) \u22c1 Player(Anand, Chess)<\/p>\n

2. \u00acPlayer (Jay, Badminton) \u22c1 Player (Saina, Badminton)<\/p>\n

 <\/p>\n

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 \u00ac Predicate \u22c1predicate will always be true. For example \u00acPlayer (Jay, Badminton) \u22c1 Player(Jay,Badminton) will always be true as Jay is either a\u00a0badminton player or he is not. Such combinations of clauses which are already true are eliminated\u00a0from the resolved clauses. And thus the resultant clause in above case is\u00a0Player(Anand, Chess) \u22c1 Player (Saina, Badminton)\u00a0In other words, during resolution, if there are two literals with same value and opposite sign, they\u00a0<\/em>a<\/em>r<\/em>e eliminated from the resultant clause.<\/em><\/p>\n

 <\/p>\n

This process becomes little complicated when the variables are used. For example if we have two clauses<\/p>\n

 <\/p>\n

Man (Ramji)<\/p>\n

\u00acMan(X) \u22c1Person (X)<\/p>\n

 <\/p>\n

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 \u00acMan(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.<\/p>\n

 <\/p>\n

Producing a proof<\/strong><\/p>\n

 <\/p>\n

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.<\/p>\n

 <\/p>\n

For example if we want to prove Relief (Government, Ramji), what we will do is to add another<\/p>\n

statement to the list of clauses<\/p>\n

\u00acRelief (Government, Ramji)<\/p>\n

 <\/p>\n

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\u00a0must 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.<\/span><\/p>\n<\/div>\n

\n

 <\/p>\n

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.<\/p>\n

 <\/p>\n

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\u00a0\u00acBuildHouse(H) \u22c1Lost(X,H,2000) as one of the clause, and if we have one more clause in the\u00a0premise \u00a0as \u00a0BuildHouse(H) as \u00a0one part, \u00a0it \u00a0is \u00a0highly recommended\u00a0 to \u00a0use \u00a0that \u00a0clause \u00a0as\u00a0another parent. It is because \u00acBuildHouse and BuildHouse will cancel each other out in the\u00a0resolvent.<\/p>\n

 <\/p>\n

3. Choose \u00a0other \u00a0parent \u00a0clause \u00a0which \u00a0is \u00a0as \u00a0short \u00a0as \u00a0possible. \u00a0This \u00a0will \u00a0reduce \u00a0the \u00a0size \u00a0of resultant clause and improves the chances of getting to a null clause.<\/p>\n

 <\/p>\n

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.<\/p>\n

 <\/p>\n

Proving using resolutionLet us pick up example 25.1<\/p>\n

 <\/p>\n

1. Man (Ramji)<\/p>\n

2. Farmer (Ramji)<\/p>\n

3. \u2200??Kuchchhi(X) \u2192 Gujrati (X)<\/p>\n

4. Belongsto (Ramji, Bhachau)<\/p>\n

5. \u2200??\u2203??Person(X) \u22c0Belongsto (X,Bhachau) \u22c0 House (H,X) \u2192 Lost (X,H,2000)<\/p>\n

6. \u2200??\u2203??Person(X) \u22c0 House (H,X) \u22c0 Lost (X,H,2000) \u2192 Relief (Government, X)<\/p>\n

7.\u00a0 \u2200??Man(X) \u2192 Person(X)<\/p>\n

8. \u2203??House (H,Ramji)<\/p>\n

 <\/p>\n

Converting them to a clausal form yields following.<\/p>\n

 <\/p>\n

1. Man(Ramji)<\/p>\n

2. Farmer(Ramji)<\/p>\n

3. \u00acKuchchhi(X) \u22c1Gujrati (X)<\/p>\n

4. Belongto (Ramji, Bhachau)<\/p>\n

5. \u00acPerson(X) \u22c1\u00acBelongsto (X,Bhachau) \u22c1\u00acHouse (Houseof(X),X) \u22c1 Lost (X,Hosueof(X),2000)<\/p>\n

6. \u00acPerson(X) \u22c1\u00acHouse (Houseof(X),X) \u22c1\u00acLost (X,Houseof(X),2000) \u22c1Relief (Government, X)<\/p>\n

7. \u00ac Man(X) \u22c1 Person(X)<\/p>\n

8. House(Houseof(Ramji), Ramji)<\/p>\n

 <\/p>\n

Now let us pick up what we want to prove. Ramji received a relief from the government.<\/p>\n

 <\/p>\n

9. \u00acRelief (Government, Ramji)<\/p>\n<\/div>\n

\n

\"\"<\/p>\n<\/div>\n

\n

F<\/em>i<\/em>gu<\/em>re 26.1 The resolution process<\/em><\/p>\n

 <\/p>\n

The complete resolution process is depicted in the figure 26.1.<\/p>\n<\/div>\n

 <\/p>\n

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

\n

 <\/p>\n

Let us take another example to reiterate.<\/p>\n

 <\/p>\n

1. Man(Ramji)<\/p>\n

2. Farmer(Ramji)<\/p>\n

3. Belongto (Ramji, Bhachau)<\/p>\n

4. \u2200??\u2203??Person(X) \u22c0Belongsto (X, Bhachau) \u22c0 House (H,X) \u2192 Lost (X,H,2000)<\/p>\n

5. \u2200??\u2200??\u2203??Person(X) \u22c0 House (H,X) \u22c0 Lost (X,H,2000) \u2192 Relief (Government, X)<\/p>\n

6. \u2203??BuildHouse (H, Ramji, 2003)\u22c0 \u00ac Changedhouse(Ramji,H,2015)<\/p>\n

7.\u00a0 \u2200??\u2200??1\u2200??2\u2200??3\u2203??Buildhouse(H,X,T1)\u22c0\u00ac Changedhouse(X,H,T2)\u00a0 \u00a0\u22c0\u00a0 \u00a0Between(T3,T1,T2)<\/p>\n

\u2192Liveinhouse(H,X,T3)<\/p>\n

 <\/p>\n

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

 <\/p>\n

8. \u00acLiveinhouse(H,Ramji,2010)<\/p>\n

 <\/p>\n

Now, let us convert these statements into clausal forms.<\/p>\n

 <\/p>\n

1. Man(Ramji)<\/p>\n

2. Farmer(Ramji)<\/p>\n

3. Belongto (Ramji, Bhachau)<\/p>\n

4. \u00acPerson(X) \u22c1\u00acBelongsto (X,Bhachau) \u22c1\u00acHouse (Houseof(X),X) \u22c1 Lost (X,Hosueof(X),2000)<\/p>\n

5. \u00acPerson(X) \u22c1\u00acHouse (,X) \u22c1\u00acLost (X,Houseof(X),2000) \u22c1Relief (Government, X)<\/p>\n

6. BuildHouse (Houseof(Ramji), Ramji, 2003)<\/p>\n

7. \u00ac Changedhouse(Ramji, Houseof(Ramji),2015)<\/p>\n

8. \u00ac Buildhouse(Houseof(Ramji),Ramji,T1)\u22c1Changedhouse(Ramji, Houseof(Ramji),T2)<\/p>\n

\u22c1\u00ac Between(T3,T1,T2) \u22c1Liveinhouse(Houseof(Ramji),Ramji,T3)<\/p>\n

9. \u00acLiveinhouse(Houseof(Ramji),Ramji,2010)<\/p>\n

 <\/p>\n

Note that statement no. 6 is divided into\u00a0 two clauses connected by and thus the step<\/p>\n

number 8 is applied.<\/p>\n

 <\/p>\n

The resolution process is depicted in figure 26.2.<\/p>\n

 <\/p>\n

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.<\/p>\n

 <\/p>\n

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.<\/p>\n<\/div>\n

\"\"<\/p>\n

F<\/em>i<\/em>gu<\/em>re 26.2 The resolution process for predicates with function<\/em><\/p>\n

 <\/p>\n

Summary<\/strong><\/p>\n

 <\/p>\n

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 \u22c0 and then write them as separate rules. The last step is to standardize the variables\u00a0apart. Once all these steps are applied, all wffs are converted to clausal form. Once converted to\u00a0clausal 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.<\/p>\n\n\n\n
you can view video on Resolution<\/strong><\/td>\n\"\"<\/a><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n","protected":false},"author":4,"menu_order":26,"template":"","meta":{"_acf_changed":false,"pb_show_title":"on","pb_short_title":"","pb_subtitle":"","pb_authors":["prof-bhushan-trivedi"],"pb_section_license":""},"chapter-type":[],"contributor":[58],"license":[],"class_list":["post-217","chapter","type-chapter","status-publish","hentry","contributor-prof-bhushan-trivedi"],"part":3,"_links":{"self":[{"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/pressbooks\/v2\/chapters\/217","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/pressbooks\/v2\/chapters"}],"about":[{"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/wp\/v2\/types\/chapter"}],"author":[{"embeddable":true,"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/wp\/v2\/users\/4"}],"version-history":[{"count":6,"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/pressbooks\/v2\/chapters\/217\/revisions"}],"predecessor-version":[{"id":485,"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/pressbooks\/v2\/chapters\/217\/revisions\/485"}],"part":[{"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/pressbooks\/v2\/parts\/3"}],"metadata":[{"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/pressbooks\/v2\/chapters\/217\/metadata\/"}],"wp:attachment":[{"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/wp\/v2\/media?parent=217"}],"wp:term":[{"taxonomy":"chapter-type","embeddable":true,"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/pressbooks\/v2\/chapter-type?post=217"},{"taxonomy":"contributor","embeddable":true,"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/wp\/v2\/contributor?post=217"},{"taxonomy":"license","embeddable":true,"href":"https:\/\/ebooks.inflibnet.ac.in\/itp6\/wp-json\/wp\/v2\/license?post=217"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}