Scribd Logo
Upload

Welcome to Scribd!

  • 29 views

    Resolution Method in Ai: Assistant Proof. Dr. Emad I Abdul Kareem

    Uploaded by

    Sahil Shaikh
    The document discusses resolution method in artificial intelligence. Resolution method is an inference rule used in propositional and first-order predicate logic to prove the satisfiability of a statement. It uses a technique called proof by refutation. The key idea is to use the knowledge base and negated goal to obtain a null clause, indicating a contradiction. This proves the original goal is true. The document provides examples of converting statements to conjunctive normal form and applying resolution method to prove a goal statement.

    Copyright:

    © All Rights Reserved
    Download as PPTX, PDF, TXT or read online from Scribd

    Resolution Method in Ai: Assistant Proof. Dr. Emad I Abdul Kareem

    Uploaded by

    Sahil Shaikh
    29 views12 pages
    The document discusses resolution method in artificial intelligence. Resolution method is an inference rule used in propositional and first-order predicate logic to prove the satisfiability of a statement. It uses a technique called proof by refutation. The key idea is to use the knowledge base and negated goal to obtain a null clause, indicating a contradiction. This proves the original goal is true. The document provides examples of converting statements to conjunctive normal form and applying resolution method to prove a goal statement.

    Original Title

    9_2020_03_28!05_31_28_PM.pptx

    Copyright

    © © All Rights Reserved

    Available Formats

    PPTX, PDF, TXT or read online from Scribd

    Did you find this document useful?

    Is this content inappropriate?

    The document discusses resolution method in artificial intelligence. Resolution method is an inference rule used in propositional and first-order predicate logic to prove the satisfiability of a statement. It uses a technique called proof by refutation. The key idea is to use the knowledge base and negated goal to obtain a null clause, indicating a contradiction. This proves the original goal is true. The document provides examples of converting statements to conjunctive normal form and applying resolution method to prove a goal statement.

    Copyright:

    © All Rights Reserved
    Download as PPTX, PDF, TXT or read online from Scribd
    Download as pptx, pdf, or txt
    29 views12 pages

    Resolution Method in Ai: Assistant Proof. Dr. Emad I Abdul Kareem

    Uploaded by

    Sahil Shaikh
    The document discusses resolution method in artificial intelligence. Resolution method is an inference rule used in propositional and first-order predicate logic to prove the satisfiability of a statement. It uses a technique called proof by refutation. The key idea is to use the knowledge base and negated goal to obtain a null clause, indicating a contradiction. This proves the original goal is true. The document provides examples of converting statements to conjunctive normal form and applying resolution method to prove a goal statement.

    Copyright:

    © All Rights Reserved
    Download as PPTX, PDF, TXT or read online from Scribd
    Download as pptx, pdf, or txt
    You are on page 1of 12

    RESOLUTION METHOD

    IN AI

    Assistant proof. Dr. Emad I Abdul Kareem


    RESOLUTION METHOD IN AI
    Resolution method is an inference rule which is used in both Propositional as well
    as First-order Predicate Logic in different ways. This method is basically used for
    proving the satisfiability of a sentence. In resolution method, we use Proof by
    Refutation technique to prove the given statement.
    The key idea for the resolution method is to use the knowledge base and negated
    goal to obtain null clause (which indicates contradiction). Resolution method is also
    called Proof by Refutation. Since the knowledge base itself is consistent, the
    contradiction must be introduced by a negated goal. As a result, we have to conclude
    that the original goal is true.
    RESOLUTION METHOD IN
    PROPOSITIONAL LOGIC
    In propositional logic, resolution method is the only inference rule which gives a
    new clause when two or more clauses are coupled together. Using propositional
    resolution, it becomes easy to make a theorem prover sound and complete for all. The
    process followed to convert the propositional logic into resolution method contains the
    below steps:
    • Convert the given statements into clausal form,
    • Apply and proof the given goal using negation rule.
    • Use those literals which are needed to prove.
    • Solve the clauses together and achieve the goal.
    But, before solving problems using Resolution method, let’s understand two
    normal forms
    CONVERT THE GIVEN STATEMENTS
    INTO CLAUSAL FORM ( CONJUNCTIVE
    NORMAL FORM(CNF))
    ∀x [B(x) → (∃y [Q(x, y) ∧ ⌐ P(y)]
    ∧ ⌐ ∃y [Q(x, y) ∧ Q(y, x)]
    ∧ ∀y [⌐ B(y) → ⌐ E(x, y)])]

    1- Eliminate the implication (→)


    E1 → E2 = ⌐ E1 ∨ E2
    ∀x [⌐ B(x) ∨ ( ∃y [ Q(x ,y) ∧ ⌐ P(y) ] ∀x [B(x) → (∃y [Q(x, y) ∧ ⌐ P(y)]
    ∧ ⌐ ∃y [ Q(x ,y) ∧ Q(y ,x) ]
    ∧ ∀y [⌐(⌐ B(y)) ∨ ⌐ E(x ,y)] ) ] ∧ ∀y [⌐ B(y) → ⌐ E(x, y)])]
    2- Move the negation down to the atomic formulas (by using the following rules)
    • ⌐ (P∧Q) ≡ ⌐ P ∨ ⌐ Q
    • ⌐ (P∨Q) ≡⌐P∧⌐Q
    • ⌐ (⌐ (P)) ≡ P
    • ⌐ ∀x (P (x)) ≡ ∃x (⌐ P (x))
    • ⌐ ∃x (P (x)) ≡ ∀x (⌐ P (x))

    ∀x[⌐ B(x) ∨ ( ∃y [ Q(x,y) ∧ ⌐ P(y) ]


    ∧ ⌐ ∃y [ Q(x ,y) ∧ Q(y ,x) ]
    ∧ ∀y [ ⌐ Q(x,y) ∨ ⌐ Q(y,x) ]
    ∧ ∀y [ B(y) ∨ ⌐ E(x,y)] ) ] ∧ ∀y [⌐(⌐ B(y)) ∨ ⌐ E(x ,y)] ) ]

    3- Purge existential quantifiers


    The function that is eliminate the existential are called “Skolem function”
    ∀x[⌐ B(x) ∨ ( [ Q(x , f (x)) ∧ ⌐ P(f (x)) ] ∀x[⌐ B(x) ∨ ( ∃y [ Q(x,y) ∧ ⌐ P(y) ]

    ∧ ∀y [ ⌐ Q(x,y) ∨ ⌐ Q(y,x) ]
    ∧ ∀y [ B(y) ∨ ⌐ E(x,y)] ) ]
    4- Rename variables, as necessary, so that no two variables are the same.
    ∀x[⌐ B(x) ∨ ( [ Q(x , f (x)) ∧ ⌐ P(f (x)) ]
    ∧ ∀y [ ⌐ Q(x,y) ∨ ⌐ Q(y,x) ]
    ∧ ∀z [ B(z) ∨ ⌐ E(x,z)] ) ] ∧ ∀y [ B(y) ∨ ⌐ E(x,y)] ) ]

    5- Move the Universal quantifiers to the left of the statement.


    ∀x ∀y ∀z [⌐ B(x) ∨ ( [ Q(x , f (x)) ∧ ⌐ P(f (x)) ] ∀x[⌐ B(x) ∨ ( [ Q(x , f (x)) ∧ ⌐ P(f (x)) ]
    ∧ ∀y [ ⌐ Q(x,y) ∨ ⌐ Q(y,x) ]
    ∧ [ ⌐ Q(x,y) ∨ ⌐ Q(y,x) ] ∧ ∀z [ B(z) ∨ ⌐ E(x,z)] ) ]
    ∧ [ B(z) ∨ ⌐ E(x,z)] ) ]
    6- Move the disjunction down to the literals, using distributive laws
    E1 ∨ (E2 ∧ E3 ∧ E4 ∧…) ≡ (E1 ∨ E2) ∧ (E1∨E3) ∧ ….
    E1 ∧ (E2 ∨ E3 ∨ E4∨…) ≡ (E1 ∧ E2) ∨ (E1∧E3) ∨ ….
     
     
    ∀x ∀y ∀z [ ( ⌐ B(x) ∨ ( Q(x , f (x)) ∀x ∀y ∀z [⌐ B(x) ∨ ( [ Q(x , f (x)) ∧ ⌐ P(f (x)) ]
    ∧ ( ⌐ B(x) ∨ ⌐ P(f (x) ) ) ∧ [ ⌐ Q(x,y) ∨ ⌐ Q(y,x) ]
    ∧ [ B(z) ∨ ⌐ E(x,z)] ) ]
    ∧ ( ⌐ B(x) ∨ ⌐ Q(x,y) ∨ ⌐ Q(y,x) )
    ∧ (⌐ B(x) ∨ B(z) ∨ ⌐ E(x,z) ) ]
     
    7- Eliminate the conjunctions
    ∀x ∀y ∀z [ ( ⌐ B(x) ∨ ( Q(x , f (x))
    ∀x [ ⌐ B(x) ∨ ( Q(x , f (x) ]
    ∧ ( ⌐ B(x) ∨ ⌐ P(f (x) ) )
    ∀x [⌐ B(x) ∨ ⌐ P(f (x) ) ] ∧ ( ⌐ B(x) ∨ ⌐ Q(x,y) ∨ ⌐ Q(y,x) )
    ∧ (⌐ B(x) ∨ B(z) ∨ ⌐ E(x,z) ) ]
    ∀x ∀y [ ⌐ B(x) ∨ ⌐ Q(x,y) ∨ ⌐ Q(y,x) ]
    ∀x ∀z [⌐ B(x) ∨ B(z) ∨ ⌐ E(x,z) ]
    8- Rename all the variables, as necessary, so that no two variables are the same.
    ∀x [ ⌐ B(x) ∨ ( Q(x , f (x) ] ∀x [ ⌐ B(x) ∨ ( Q(x , f (x) ]
    ∀w [⌐ B(w) ∨ ⌐ P(f (w) ) ] ∀x [⌐ B(x) ∨ ⌐ P(f (x) ) ]
    ∀x ∀y [ ⌐ B(x) ∨ ⌐ Q(x,y) ∨ ⌐ Q(y,x) ]
    ∀u ∀y [⌐ B(u) ∨ ⌐ Q(u,y) ∨ ⌐ Q(y,u) ] ∀x ∀z [⌐ B(x) ∨ B(z) ∨ ⌐ E(x,z) ]
    ∀a ∀z [⌐ B(a) ∨ B(z) ∨ ⌐ E(a,z) ]

    9- Purge the universal quantifiers.


    ∀x [ ⌐ B(x) ∨ ( Q(x , f (x) ]
    ⌐ B(x) ∨ ( Q(x , f (x)) ∀x [⌐ B(x) ∨ ⌐ P(f (x) ) ]
    ⌐ B(w) ∨ ⌐ P(f (w) ) ∀x ∀y [ ⌐ B(x) ∨ ⌐ Q(x,y) ∨ ⌐ Q(y,x) ]
    ∀x ∀z [⌐ B(x) ∨ B(z) ∨ ⌐ E(x,z) ]
    ⌐ B(u) ∨ ⌐ Q(u,y) ∨ ⌐ Q(y,u)
    ⌐ B(a) ∨ B(z) ∨ ⌐ E(a,z) )
    EXAMPLE
    Consider the following Knowledge Base:
    The humidity is high or the sky is cloudy. ‫ائمة‬I‫لسماء غ‬II‫لية أو ا‬II‫ا‬I‫لرطوبة ع‬II‫ا‬.
    If the sky is cloudy, then it will rain. ‫مطر‬III‫سوفت‬III‫ ف‬، ‫ائمة‬I‫لسماء غ‬II‫انتا‬I‫إذا ك‬.
    If the humidity is high, then it is hot. ‫ارا‬I‫لطقسح‬II‫كونا‬II‫ ي‬I‫م‬III‫ ث‬،‫لية‬II‫ا‬I‫لرطوبة ع‬II‫انتا‬I‫إذا ك‬.
    It is not hot. ‫ارا‬I‫يس ح‬II‫لطقسل‬II‫ا‬.
    Goal: It will rain.
    Use propositional logic and apply resolution method to prove that the goal is derivable from the
    given knowledge base.
    Solution: Let’s construct propositions of the given sentences one by one:
     
    1) Let,
    The humidity is high or the sky is cloudy
    P: Humidity is high.
         Q: Sky is cloudy.
    It will be represented as P V Q.
     
    2) If the sky is cloudy, then it will rain
    Q: Sky is cloudy.                      …from (1)
    Let, R: It will rain.
    It will be represented as Q → R.
     
    3) If the humidity is high, then it is hot.
    P: Humidity is high.                 …from (1)
    Let, S: It is hot.
    It will be represented as P →   S.
     
    4) ¬S: It is not hot.
    Applying resolution method:
    1. P V Q.
    2. Q → R.
    In (2), Q → R will be converted as (¬Q V R)

    3. P →   S.
    In (3), P →  S will be converted as (¬P V S)

    4. ¬S.

    Negation of Goal (¬R): It will not rain.

    Finally, apply the rule as shown below:


    The End

    You might also like