Ai lecture 13(unit03)

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. 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 : Rimi is Hungry If R imi is hungry she barks 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 : Rimi is Hungry If R imi is hungry she barks 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 . Hungry( Rimi ) hungry( Rimi ) ->barks( Rimi ) barks( Rimi ) ->angry(Raja)

4. Resolution in FOL Hungry( Rimi ) hungry( Rimi ) ->barks( Rimi ) 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. Hungry( Rimi ) ~ hungry( Rimi ) V barks( Rimi ) ~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. Hungry( Rimi ) ~hungry( Rimi ) V barks( Rimi ) ~barks( Rimi ) V angry(Raja ) ~Angry(Raja

7. Resolution in FOL Step-4: Draw Resolution graph: Hungry( Rimi ) ~hungry( Rimi ) V barks( Rimi ) ~barks( Rimi ) V angry(Raja ) ~Angry(Raja

8. Proof By Resolution In FOL Examples Resolution in FOL: Example Example : All people who are graduating are happy All happy people smile 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 : All people who are graduating are happy All happy people smile 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 . ∀ x∃x ∀x : graduating(x)->happy(x) ∀ x: happy(x) ->smile(x) ∃x : graduating(x) ∃ x: smiling(x)

10. Resolution in FOL ∀x : graduating(x)->happy(x) ∀x: happy(x) ->smile(x) ∃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. ~ graduating(x) V happy(x ) ~ happy(x1) V smile(x1) 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. ~ graduating(x) V happy(x) ~ happy(x1) V smile(x1) graduating(x2) ~ smiling(x3)

13. Resolution in FOL Step-4: Draw Resolution graph: ~ graduating(x) V happy(x ) ~ happy(x1) V smile(x1 ) graduating(x2) ~ smiling(x3)