Proof by contradiction,ie. Resolution algorithm (-BaV Rav(-Pav B)A(-PuvBa) 4.Apply(ver)and flatten: (BV Rav((-R)vB) 3.uing de Morgan's and double-negation 电y (B (PaB))((P)BL) Conversion to CNF :：wh < Resolution .. -inference:deriving fro Resolution example ... 国Resolution Conjunctive Normal Form (CNF—universal) conjunction of disjunctions of literals | {z } clauses E.g., (A ∨ ¬B) ∧ (B ∨ ¬C ∨ ¬D) Resolution inference rule (for CNF): complete for propositional logic `1 ∨ · · · ∨ `k, m1 ∨ · · · ∨ mn `1 ∨ · · · ∨ `i−1 ∨ `i+1 ∨ · · · ∨ `k ∨ m1 ∨ · · · ∨ mj−1 ∨ mj+1 ∨ · · · ∨ mn where `i and mj are complementary literals. E.g., OK OK OK A A B P? P? A S OK P W A P1,3 ∨ P2,2, ¬P2,2 P1,3 Resolution is sound and complete for propositional logic Chapter 7 67 Conversion to CNF B1,1 ⇔ (P1,2 ∨ P2,1) 1. Eliminate ⇔, replacing α ⇔ β with (α ⇒ β) ∧ (β ⇒ α). (B1,1 ⇒ (P1,2 ∨ P2,1)) ∧ ((P1,2 ∨ P2,1) ⇒ B1,1) 2. Eliminate ⇒, replacing α ⇒ β with ¬α ∨ β. (¬B1,1 ∨ P1,2 ∨ P2,1) ∧ (¬(P1,2 ∨ P2,1) ∨ B1,1) 3. Move ¬ inwards using de Morgan’s rules and double-negation: (¬B1,1 ∨ P1,2 ∨ P2,1) ∧ ((¬P1,2 ∧ ¬P2,1) ∨ B1,1) 4. Apply distributivity law (∨ over ∧) and flatten: (¬B1,1 ∨ P1,2 ∨ P2,1) ∧ (¬P1,2 ∨ B1,1) ∧ (¬P2,1 ∨ B1,1) Chapter 7 68 Resolution algorithm Proof by contradiction, i.e., show KB ∧ ¬α unsatisfiable function PL-Resolution(KB,α) returns true or false inputs: KB, the knowledge base, a sentence in propositional logic α, the query, a sentence in propositional logic clauses ← the set of clauses in the CNF representation of KB ∧ ¬α new ← { } loop do for each Ci, Cj in clauses do resolvents ←PL-Resolve(Ci ,Cj ) if resolvents contains the empty clause then return true new ← new ∪ resolvents if new ⊆ clauses then return false clauses ← clauses ∪new Chapter 7 69 Resolution example KB = (B1,1 ⇔ (P1,2 ∨ P2,1)) ∧ ¬B1,1 α = ¬P1,2 P1,2 P1,2 P2,1 P1,2 B1,1 B1,1 P2,1 B1,1 P1,2 P2,1 P2,1 P1,2 B1,1 B1,1 P1,2 B1,1 P2,1 B1,1 P2,1 B1,1 P1,2 P2,1 P1,2 Chapter 7 70 Summary Logical agents apply inference to a knowledge base to derive new information and make decisions Basic concepts of logic: – syntax: formal structure of sentences – semantics: truth of sentences wrt models – entailment: necessary truth of one sentence given another – inference: deriving sentences from other sentences – soundess: derivations produce only entailed sentences – completeness: derivations can produce all entailed sentences Wumpus world requires the ability to represent partial and negated informa￾tion, reason by cases, etc. Forward, backward chaining are linear-time, complete for Horn clauses Resolution is complete for propositional logic Propositional logic lacks expressive power Chapter 7 71