{"id":2294,"date":"2022-04-16T19:11:30","date_gmt":"2022-04-16T19:11:30","guid":{"rendered":"https:\/\/mdr.foobrdigital.com\/?p=2294"},"modified":"2022-04-16T19:11:30","modified_gmt":"2022-04-16T19:11:30","slug":"resolution-in-fol","status":"publish","type":"post","link":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/2022\/04\/16\/resolution-in-fol\/","title":{"rendered":"Resolution in FOL"},"content":{"rendered":"\n

Resolution<\/h2>\n\n\n\n

Resolution is a theorem proving technique that proceeds by building refutation proofs, i.e., proofs by contradictions. It was invented by a Mathematician John Alan Robinson in the year 1965.<\/p>\n\n\n\n

Resolution is used, if there are various statements are given, and we need to prove a conclusion of those statements. Unification is a key concept in proofs by resolutions. Resolution is a single inference rule which can efficiently operate on the conjunctive normal form or clausal form<\/strong>.<\/p>\n\n\n\n

Clause<\/strong>: Disjunction of literals (an atomic sentence) is called a clause<\/strong>. It is also known as a unit clause.<\/p>\n\n\n\n

Conjunctive Normal Form<\/strong>: A sentence represented as a conjunction of clauses is said to be conjunctive normal form<\/strong> or CNF<\/strong>.<\/p>\n\n\n\n

Note: To better understand this topic, firstly learns the FOL in AI.<\/h4>\n\n\n\n

The resolution inference rule:<\/h2>\n\n\n\n

The resolution rule for first-order logic is simply a lifted version of the propositional rule. Resolution can resolve two clauses if they contain complementary literals, which are assumed to be standardized apart so that they share no variables.<\/p>\n\n\n\n

\"Resolution<\/figure>\n\n\n\n

Where li<\/sub><\/strong> and mj<\/sub><\/strong> are complementary literals.<\/p>\n\n\n\n

This rule is also called the binary resolution rule<\/strong> because it only resolves exactly two literals.<\/p>\n\n\n\n

Example:<\/h3>\n\n\n\n

We can resolve two clauses which are given below:<\/p>\n\n\n\n

[Animal (g(x) V Loves (f(x), x)]       and       [\uffe2 Loves(a, b) V \uffe2Kills(a, b)]<\/strong><\/p>\n\n\n\n

Where two complimentary literals are: Loves (f(x), x) and \uffe2 Loves (a, b)<\/strong><\/p>\n\n\n\n

These literals can be unified with unifier \u03b8= [a\/f(x), and b\/x] <\/strong>, and it will generate a resolvent clause:<\/p>\n\n\n\n

[Animal (g(x) V \uffe2 Kills(f(x), x)].<\/strong><\/p>\n\n\n\n

Steps for Resolution:<\/h2>\n\n\n\n
  1. Conversion of facts into first-order logic.<\/li>
  2. Convert FOL statements into CNF<\/li>
  3. Negate the statement which needs to prove (proof by contradiction)<\/li>
  4. Draw resolution graph (unification).<\/li><\/ol>\n\n\n\n

    To better understand all the above steps, we will take an example in which we will apply resolution.<\/p>\n\n\n\n

    Example:<\/h3>\n\n\n\n
    1. John likes all kind of food.<\/strong><\/li>
    2. Apple and vegetable are food<\/strong><\/li>
    3. Anything anyone eats and not killed is food.<\/strong><\/li>
    4. Anil eats peanuts and still alive<\/strong><\/li>
    5. Harry eats everything that Anil eats.<\/strong>
      Prove by resolution that:<\/strong><\/li>
    6. John likes peanuts.<\/strong><\/li><\/ol>\n\n\n\n

      Step-1: Conversion of Facts into FOL<\/strong><\/p>\n\n\n\n

      In the first step we will convert all the given statements into its first order logic.<\/p>\n\n\n\n

      \"Resolution<\/figure>\n\n\n\n

      Step-2: Conversion of FOL into CNF<\/strong><\/p>\n\n\n\n

      In First order logic resolution, it is required to convert the FOL into CNF as CNF form makes easier for resolution proofs.<\/p>\n\n\n\n

      • Eliminate all implication (\u2192) and rewrite<\/strong>
        1. \u2200x \u00ac food(x) V likes(John, x)<\/li>
        2. food(Apple) \u039b food(vegetables)<\/li>
        3. \u2200x \u2200y \u00ac [eats(x, y) \u039b \u00ac killed(x)] V food(y)<\/li>
        4. eats (Anil, Peanuts) \u039b alive(Anil)<\/li>
        5. \u2200x \u00ac eats(Anil, x) V eats(Harry, x)<\/li>
        6. \u2200x\u00ac [\u00ac killed(x) ] V alive(x)<\/li>
        7. \u2200x \u00ac alive(x) V \u00ac killed(x)<\/li>
        8. likes(John, Peanuts).<\/li><\/ol><\/li>
        9. Move negation (\u00ac)inwards and rewrite<\/strong>
          1. \u2200x \u00ac food(x) V likes(John, x)<\/li>
          2. food(Apple) \u039b food(vegetables)<\/li>
          3. \u2200x \u2200y \u00ac eats(x, y) V killed(x) V food(y)<\/li>
          4. eats (Anil, Peanuts) \u039b alive(Anil)<\/li>
          5. \u2200x \u00ac eats(Anil, x) V eats(Harry, x)<\/li>
          6. \u2200x \u00ackilled(x) ] V alive(x)<\/li>
          7. \u2200x \u00ac alive(x) V \u00ac killed(x)<\/li>
          8. likes(John, Peanuts).<\/li><\/ol><\/li>
          9. Rename variables or standardize variables<\/strong>
            1. \u2200x \u00ac food(x) V likes(John, x)<\/li>
            2. food(Apple) \u039b food(vegetables)<\/li>
            3. \u2200y \u2200z \u00ac eats(y, z) V killed(y) V food(z)<\/li>
            4. eats (Anil, Peanuts) \u039b alive(Anil)<\/li>
            5. \u2200w\u00ac eats(Anil, w) V eats(Harry, w)<\/li>
            6. \u2200g \u00ackilled(g) ] V alive(g)<\/li>
            7. \u2200k \u00ac alive(k) V \u00ac killed(k)<\/li>
            8. likes(John, Peanuts).<\/li><\/ol><\/li>
            9. Eliminate existential instantiation quantifier by elimination.<\/strong>
              In this step, we will eliminate existential quantifier \u2203, and this process is known as Skolemization<\/strong>. But in this example problem since there is no existential quantifier so all the statements will remain same in this step.<\/li>
            10. Drop Universal quantifiers.<\/strong>
              In this step we will drop all universal quantifier since all the statements are not implicitly quantified so we don’t need it.
              1. \u00ac food(x) V likes(John, x)<\/li>
              2. food(Apple)<\/li>
              3. food(vegetables)<\/li>
              4. \u00ac eats(y, z) V killed(y) V food(z)<\/li>
              5. eats (Anil, Peanuts)<\/li>
              6. alive(Anil)<\/li>
              7. \u00ac eats(Anil, w) V eats(Harry, w)<\/li>
              8. killed(g) V alive(g)<\/li>
              9. \u00ac alive(k) V \u00ac killed(k)<\/li>
              10. likes(John, Peanuts).<\/li><\/ol><\/li><\/ul>\n\n\n\n

                Note: Statements “food(Apple) \u039b food(vegetables)” and “eats (Anil, Peanuts) \u039b alive(Anil)” can be written in two separate statements.<\/h4>\n\n\n\n
                • Distribute conjunction \u2227 over disjunction \u00ac.<\/strong>
                  This step will not make any change in this problem.<\/li><\/ul>\n\n\n\n

                  Step-3: Negate the statement to be proved<\/strong><\/p>\n\n\n\n

                  In this statement, we will apply negation to the conclusion statements, which will be written as \u00aclikes(John, Peanuts)<\/p>\n\n\n\n

                  Step-4: Draw Resolution graph:<\/strong><\/p>\n\n\n\n

                  Now in this step, we will solve the problem by resolution tree using substitution. For the above problem, it will be given as follows:<\/p>\n\n\n\n

                  \"Resolution<\/figure>\n\n\n\n

                  Hence the negation of the conclusion has been proved as a complete contradiction with the given set of statements.<\/p>\n\n\n\n

                  Explanation of Resolution graph:<\/h2>\n\n\n\n
                  • In the first step of resolution graph, \u00aclikes(John, Peanuts) <\/strong>, and likes(John, x) <\/strong>get resolved(canceled) by substitution of {Peanuts\/x}<\/strong>, and we are left with \u00ac food(Peanuts)<\/strong><\/li>
                  • In the second step of the resolution graph, \u00ac food(Peanuts) <\/strong>, and food(z) <\/strong>get resolved (canceled) by substitution of { Peanuts\/z}<\/strong>, and we are left with \u00ac eats(y, Peanuts) V killed(y) <\/strong>.<\/li>
                  • In the third step of the resolution graph, \u00ac eats(y, Peanuts) <\/strong>and eats (Anil, Peanuts) <\/strong>get resolved by substitution {Anil\/y}<\/strong>, and we are left with Killed(Anil) <\/strong>.<\/li>
                  • In the fourth step of the resolution graph, Killed(Anil) <\/strong>and \u00ac killed(k) <\/strong>get resolve by substitution {Anil\/k}<\/strong>, and we are left with \u00ac alive(Anil) <\/strong>.<\/li>
                  • In the last step of the resolution graph \u00ac alive(Anil) <\/strong>and alive(Anil) <\/strong>get resolved.<\/li><\/ul>\n","protected":false},"excerpt":{"rendered":"

                    Resolution Resolution is a theorem proving technique that proceeds by building refutation proofs, i.e., proofs by contradictions. It was invented by a Mathematician John Alan Robinson in the year 1965. Resolution is used, if there are various statements are given, and we need to prove a conclusion of those statements. Unification is a key concept […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[885],"tags":[],"_links":{"self":[{"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/posts\/2294"}],"collection":[{"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/comments?post=2294"}],"version-history":[{"count":0,"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/posts\/2294\/revisions"}],"wp:attachment":[{"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/media?parent=2294"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/categories?post=2294"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/mudassirbackup.infinitycodestudio.com\/index.php\/wp-json\/wp\/v2\/tags?post=2294"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}