[ A)De Morgan 8 c double-negation eliminatio Logical equivalence O[2)for n symbok;probkem is co-NP-complete TT-CnEcK-A.modd)returns tme fals Depth-first enumeration ofall models is sound and complete Inference by enumeration Truth tables for inference Modus Ponens(for Horn Form):complete for Hor KBs Forward and backward chaining enumeration (al -Typically require translation of sentences into a normal orm rC Ca Proof methods ntenceissiable ifit is true inme mode A sentence is valid if it is true in all modeb, Validity and satisfiability 。 Truth tables for inference B1,1 B2,1 P1,1 P1,2 P2,1 P2,2 P3,1 R1 R2 R3 R4 R5 KB false false false false false false false true true true true false false false false false false false false true true true false true false false . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . false true false false false false false true true false true true false false true false false false false true true true true true true true false true false false false true false true true true true true true false true false false false true true true true true true true true false true false false true false false true false false true true false . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . true true true true true true true false true true false true false Enumerate rows (different assignments to symbols), if KB is true in row, check that α is too Chapter 7 37 Inference by enumeration Depth-first enumeration of all models is sound and complete function TT-Entails?(KB,α) returns true or false inputs: KB, the knowledge base, a sentence in propositional logic α, the query, a sentence in propositional logic symbols ← a list of the proposition symbols in KB and α return TT-Check-All(KB,α,symbols, [ ]) function TT-Check-All(KB,α,symbols, model) returns true or false if Empty?(symbols) then if PL-True?(KB, model) then return PL-True?(α, model) else return true else P do ← First(symbols); rest ← Rest(symbols) return TT-Check-All(KB,α, rest,Extend(P,true, model)) and TT-Check-All(KB,α, rest,Extend(P,false, model)) O(2 n ) for n symbols; problem is co-NP-complete Chapter 7 38 Logical equivalence Two sentences are logically equivalent iff true in same models: α ≡ β if and only if α |= β and β |= α (α ∧ β) ≡ (β ∧ α) commutativity of ∧ (α ∨ β) ≡ (β ∨ α) commutativity of ∨ ((α ∧ β) ∧ γ) ≡ (α ∧ (β ∧ γ)) associativity of ∧ ((α ∨ β) ∨ γ) ≡ (α ∨ (β ∨ γ)) associativity of ∨ ¬(¬α) ≡ α double-negation elimination (α ⇒ β) ≡ (¬β ⇒ ¬α) contraposition (α ⇒ β) ≡ (¬α ∨ β) implication elimination (α ⇔ β) ≡ ((α ⇒ β) ∧ (β ⇒ α)) biconditional elimination ¬(α ∧ β) ≡ (¬α ∨ ¬β) De Morgan ¬(α ∨ β) ≡ (¬α ∧ ¬β) De Morgan (α ∧ (β ∨ γ)) ≡ ((α ∧ β) ∨ (α ∧ γ)) distributivity of ∧ over ∨ (α ∨ (β ∧ γ)) ≡ ((α ∨ β) ∧ (α ∨ γ)) distributivity of ∨ over ∧ Chapter 7 39 Validity and satisfiability A sentence is valid if it is true in all models, e.g., True, A ∨ ¬A, A ⇒ A, (A ∧ (A ⇒ B)) ⇒ B Validity is connected to inference via the Deduction Theorem: KB |= α if and only if (KB ⇒ α) is valid A sentence is satisfiable if it is true in some model e.g., A ∨ B, C A sentence is unsatisfiable if it is true in no models e.g., A ∧ ¬A Satisfiability is connected to inference via the following: KB |= α if and only if (KB ∧ ¬α) is unsatisfiable i.e., prove α by reductio ad absurdum Chapter 7 40 Proof methods Proof methods divide into (roughly) two kinds: Application of inference rules – Legitimate (sound) generation of new sentences from old – Proof = a sequence of inference rule applications Can use inference rules as operators in a standard search alg. – Typically require translation of sentences into a normal form Model checking truth table enumeration (always exponential in n) improved backtracking, e.g., Davis–Putnam–Logemann–Loveland heuristic search in model space (sound but incomplete) e.g., min-conflicts-like hill-climbing algorithms Chapter 7 41 Forward and backward chaining Horn Form (restricted) KB = conjunction of Horn clauses Horn clause = ♦ proposition symbol; or ♦ (conjunction of symbols) ⇒ symbol E.g., C ∧ (B ⇒ A) ∧ (C ∧ D ⇒ B) Modus Ponens (for Horn Form): complete for Horn KBs α1, . . . , αn, α1 ∧ · · · ∧ αn ⇒ β β Can be used with forward chaining or backward chaining. These algorithms are very natural and run in linear time Chapter 7 42