際際滷

際際滷Share a Scribd company logo

Ai lecture 13(unit03)

vikas dhakane
vikas dhakane

Knowledge Based Reasoning: Agents, Facets of Knowledge. Logic and Inferences: Formal Logic, Propositional and First Order Logic, Resolution in Propositional and First Order Logic, Deductive Retrieval, Backward Chaining, Second order Logic. Knowledge Representation: Conceptual Dependency, Frames, Semantic nets.

1 of 14
Download to read offline
Topic To Be Covered: First Order Logic(Part-04) Proof By Resolution In FOL Examples Jagdamba Education Society's SND College of Engineering & Research Centre Department of Computer Engineering SUBJECT: Artificial Intelligence & Robotics Lecture No-13(UNIT-03) Logic & Reasoning Prof.Dhakane Vikas N
Proof By Resolution In FOL Examples Resolution in FOL: Example Example: a. Rimi is Hungry b. If Rimi is hungry she barks c. If Rimi is barking then Raja is angry Prove by resolution that: Raja is angry Step-1: Conversion of Facts into FOL In the first step we will convert all the given statements into its first order logic.
Proof By Resolution In FOL Examples Resolution in FOL: Example Example: a. Rimi is Hungry b. If Rimi is hungry she barks c. If Rimi is barking then Raja is angry Prove by resolution that: Raja is angry Step-1: Conversion of Facts into FOL In the first step we will convert all the given statements into its first order logic. a. Hungry(Rimi) b. hungry(Rimi) ->barks(Rimi) c. barks(Rimi) ->angry(Raja)
Resolution in FOL a. Hungry(Rimi) b. hungry(Rimi) ->barks(Rimi) c. barks(Rimi) ->angry(Raja) Step-2: Conversion of FOL into CNF In First order logic resolution, it is required to convert the FOL into CNF as CNF form makes easier for resolution proofs. a. Hungry(Rimi) b. ~hungry(Rimi) V barks(Rimi) c. ~barks(Rimi) V angry(Raja)
Resolution in FOL Step-3: Negate the statement to be proved In this statement, we will apply negation to the conclusion statements, which will be written as ~Angry(Raja
Resolution in FOL Step-4: Draw Resolution graph: Now in this step, we will solve the problem by resolution tree using substitution. For the above problem, it will be given as follows: Hence the negation of the conclusion has been proved as a complete contradiction with the given set of statements. a. Hungry(Rimi) b. ~hungry(Rimi) V barks(Rimi) c. ~barks(Rimi) V angry(Raja) ~Angry(Raja
Resolution in FOL Step-4: Draw Resolution graph: a. Hungry(Rimi) b. ~hungry(Rimi) V barks(Rimi) c. ~barks(Rimi) V angry(Raja) ~Angry(Raja
Proof By Resolution In FOL Examples Resolution in FOL: Example Example: a. All people who are graduating are happy b. All happy people smile c. Someone is graduating Prove by resolution that: Someone is smiling Step-1: Conversion of Facts into FOL In the first step we will convert all the given statements into its first order logic.
Proof By Resolution In FOL Examples Resolution in FOL: Example Example: a. All people who are graduating are happy b. All happy people smile c. Someone is graduating Prove by resolution that: Someone is smiling Step-1: Conversion of Facts into FOL In the first step we will convert all the given statements into its first order logic. xx a. x :graduating(x)->happy(x) b. x: happy(x) ->smile(x) c. x :graduating(x) x:smiling(x)
Resolution in FOL a. x :graduating(x)->happy(x) b. x: happy(x) ->smile(x) c. x :graduating(x) x:smiling(x) Step-2: Conversion of FOL into CNF In First order logic resolution, it is required to convert the FOL into CNF as CNF form makes easier for resolution proofs. a. ~graduating(x) V happy(x) b. ~happy(x1) V smile(x1) c. graduating(x2) smiling(x3)
Resolution in FOL Step-3: Negate the statement to be proved In this statement, we will apply negation to the conclusion statements, which will be written as ~smiling(x3)
Resolution in FOL Step-4: Draw Resolution graph: Now in this step, we will solve the problem by resolution tree using substitution. For the above problem, it will be given as follows: Hence the negation of the conclusion has been proved as a complete contradiction with the given set of statements. a. ~graduating(x) V happy(x) b. ~happy(x1) V smile(x1) c. graduating(x2) ~smiling(x3)
Resolution in FOL Step-4: Draw Resolution graph: a. ~graduating(x) V happy(x) b. ~happy(x1) V smile(x1) c. graduating(x2) ~smiling(x3)
Ai lecture 13(unit03)

More Related Content

Ai lecture 13(unit03)

  • 1. Topic To Be Covered: First Order Logic(Part-04) Proof By Resolution In FOL Examples Jagdamba Education Society's SND College of Engineering & Research Centre Department of Computer Engineering SUBJECT: Artificial Intelligence & Robotics Lecture No-13(UNIT-03) Logic & Reasoning Prof.Dhakane Vikas N
  • 2. Proof By Resolution In FOL Examples Resolution in FOL: Example Example: a. Rimi is Hungry b. If Rimi is hungry she barks c. If Rimi is barking then Raja is angry Prove by resolution that: Raja is angry Step-1: Conversion of Facts into FOL In the first step we will convert all the given statements into its first order logic.
  • 3. Proof By Resolution In FOL Examples Resolution in FOL: Example Example: a. Rimi is Hungry b. If Rimi is hungry she barks c. If Rimi is barking then Raja is angry Prove by resolution that: Raja is angry Step-1: Conversion of Facts into FOL In the first step we will convert all the given statements into its first order logic. a. Hungry(Rimi) b. hungry(Rimi) ->barks(Rimi) c. barks(Rimi) ->angry(Raja)
  • 4. Resolution in FOL a. Hungry(Rimi) b. hungry(Rimi) ->barks(Rimi) c. barks(Rimi) ->angry(Raja) Step-2: Conversion of FOL into CNF In First order logic resolution, it is required to convert the FOL into CNF as CNF form makes easier for resolution proofs. a. Hungry(Rimi) b. ~hungry(Rimi) V barks(Rimi) c. ~barks(Rimi) V angry(Raja)
  • 5. Resolution in FOL Step-3: Negate the statement to be proved In this statement, we will apply negation to the conclusion statements, which will be written as ~Angry(Raja
  • 6. Resolution in FOL Step-4: Draw Resolution graph: Now in this step, we will solve the problem by resolution tree using substitution. For the above problem, it will be given as follows: Hence the negation of the conclusion has been proved as a complete contradiction with the given set of statements. a. Hungry(Rimi) b. ~hungry(Rimi) V barks(Rimi) c. ~barks(Rimi) V angry(Raja) ~Angry(Raja
  • 7. Resolution in FOL Step-4: Draw Resolution graph: a. Hungry(Rimi) b. ~hungry(Rimi) V barks(Rimi) c. ~barks(Rimi) V angry(Raja) ~Angry(Raja
  • 8. Proof By Resolution In FOL Examples Resolution in FOL: Example Example: a. All people who are graduating are happy b. All happy people smile c. Someone is graduating Prove by resolution that: Someone is smiling Step-1: Conversion of Facts into FOL In the first step we will convert all the given statements into its first order logic.
  • 9. Proof By Resolution In FOL Examples Resolution in FOL: Example Example: a. All people who are graduating are happy b. All happy people smile c. Someone is graduating Prove by resolution that: Someone is smiling Step-1: Conversion of Facts into FOL In the first step we will convert all the given statements into its first order logic. xx a. x :graduating(x)->happy(x) b. x: happy(x) ->smile(x) c. x :graduating(x) x:smiling(x)
  • 10. Resolution in FOL a. x :graduating(x)->happy(x) b. x: happy(x) ->smile(x) c. x :graduating(x) x:smiling(x) Step-2: Conversion of FOL into CNF In First order logic resolution, it is required to convert the FOL into CNF as CNF form makes easier for resolution proofs. a. ~graduating(x) V happy(x) b. ~happy(x1) V smile(x1) c. graduating(x2) smiling(x3)
  • 11. Resolution in FOL Step-3: Negate the statement to be proved In this statement, we will apply negation to the conclusion statements, which will be written as ~smiling(x3)
  • 12. Resolution in FOL Step-4: Draw Resolution graph: Now in this step, we will solve the problem by resolution tree using substitution. For the above problem, it will be given as follows: Hence the negation of the conclusion has been proved as a complete contradiction with the given set of statements. a. ~graduating(x) V happy(x) b. ~happy(x1) V smile(x1) c. graduating(x2) ~smiling(x3)
  • 13. Resolution in FOL Step-4: Draw Resolution graph: a. ~graduating(x) V happy(x) b. ~happy(x1) V smile(x1) c. graduating(x2) ~smiling(x3)