【正文】 q A B Expert Systems: Principles and Programming, Fourth Edition 51 Modus tollens p ? q conditional p q ~q converse q p inverse ~p ~q ~ p contrapositive ~q ~p Expert Systems: Principles and Programming, Fourth Edition 52 Formal Logic Proof Chip prices rise only if the yen rises. The yen rises only if the dollar falls and if the dollar falls then the yen rises. Since chip prices have risen, the dollar must have fallen. C ? Y C = chip prices rise (Y ? D) ^ (D ? Y) Y = yen rises C D = dollar falls D Expert Systems: Principles and Programming, Fourth Edition 53 Formal Logic Proof C ? Y (Y ? D) ^ (D ? Y) C D 1. C ? Y premise 2. (Y ? D) ^ (D ? Y) premise 3. C 4. Y == D 2 Equivalence 5. C ? D 1 Substitution 6. D 3,5 modus ponens Expert Systems: Principles and Programming, Fourth Edition 54 Resolution Normal form ? Conjunctive normal form (P1vP2v…)^(Q1vQ2…)^…(Z1vZ2…) ? Kowalski clausal form A1, A2, …., An ? B1, B2, …., Bm ? Horn clause A1, A2, …., An ? B Expert Systems: Principles and Programming, Fourth Edition 55 Method of Contradiction A v B (AvB)^(Av~B) A v ~B A v (B^~B) A A Expert Systems: Principles and Programming, Fourth Edition 56 Forward Reasoning T: A ? B B ? C ? CONCLUSION? C ? D A Resolve by modus ponens Expert Systems: Principles and Programming, Fourth Edition 57 Backward Reasoning What if T is very large? T may support all kinds of inferences which have nothing to do with the proof of our goal Combinational explosion ? Use Backward Reasoning Expert Systems: Principles and Programming, Fourth Edition 58 Resolution Refutation ? To refute something is to prove it false ? Refutation plete: Resolution refutation will terminate in a finite steps if there is a contradiction ? Example: Given the argument A ? B B ? C C ? D A ? D Expert Systems: Principles and Programming, Fourth Edition 59 Example A ? B B ? C C ? D A ? D To prove that A ? D is a theorem by resolution refutation: 1. A ? D equ ~A v D convert to disjunction form 2. ~(~A v D) equ A ^ ~D negate the conclusion 3. A ? B equ ~A v B B ? C equ ~B v C C ? D equ ~C v D 4. (~A v B) ^ (~B v C ) ^ (~C v D) ^ A ^ ~D resolution = nil false Expert Systems: Principles and Programming, Fourth Edition 60 Method of Contradiction A v B (AvB)^(Av~B) A v ~B A v (B^~B) A A Expert Systems: Principles and Programming, Fourth Edition 61 Propositional Logic ? Symbolic logic for manipulating proposition ? Proposition, Statement, Close sentence: a sentence whose truth value can be determined. ? Open Sentence: a sentence which contains variables ? Combinational explosion ? Can not prove argument with quantifiers Expert Systems: Principles and Programming, Fourth Edition 62 Predicate Logic ? Predicates with arguments ontopof(A, B) ? Variables and Quantifiers Universal (?x)(Rational(x) ? Real(x)) Existential (?x)(Prime(x)) ? Functions of Variables (?x)(Satellite(x)) ? (?y)(closest(y, earth)^on(y,x)) (?x)(man(x) ? mortal(x)) ^ man(Socrates) = mortal(Socrates) Expert Systems: Principles and Programming, Fourth Edition 63 Universal Quantifier ? The universal quantifier, represented by the symbol ? means “for every” or “for all”. (?x) (x is a rectangle ? x has four sides) ? The existential quantifier, represented by the symbol ? means “there exists”. (?x)