【正文】 to be proved. (1) Convert all the propositions of S to clause form. (2) Negate G and then convert into clause form, add it to the set of clauses obtained in (1). (3) Repeat until either a contradiction is found or no progress can be made: (a) Select two clauses c and c , the parent clauses. (b) Resolve c and c , the resulting clause, called the resolvent, r , will be the disjunction of all the literals of both the parent clauses with the following exception: If there are any pair of literal L and ?L, such that one of the parent clauses contains L and the other contain ?L, then delete L and ?L from the resolvent. (c) If the resolvent is the empty clause, NIL, then a contradiction has been found. If it is not, then add it to the set of clauses available to the procedure. i j ij i i j j Examples 1: Parent Clauses Resolvent p?l?m? …, ?p?n?o? … l ?m?n?o?… p, ?p?q q (MP) p?q, ?p?q q?q = q (Merge) p?q, ? p?? q q??q, p? ?p (Taotology) ?p, p NIL (Empty) ?p?q, ?q?r ?p?r (chaining) Example 2: Given Premises Convert to Clause Form p p (1) (p?q)?r ? p? ? q? r (2) (s?t) ?q ? s ? q (3) ? t ? q (4) Conclusion: t t (5) Negated Goal ? r (6) RP: (2,6) ? p ? ? q (7) (1,7) ? q (8) (4,8) ? t (9) (5,9) NIL (10) This is a contradiction among the premises and the negated conclusion. The premises are known valid. Therefore the invalid ponent must be the negated conclusion. In other words, the conclusion should be the logic consequence of the premises. 4. RP in Predicate Logic Given: a set of premises S and a conclusion G to be proved. (1) Convert S to clause form. (2) Negate G and then convert to clause form. Add it to the set of clauses obtained in (1). (3) Repeat until either a contradiction is found, or no progress can be made, or a predetermined amount of effort has been expanded: (a) Select two clauses c (x) and c (x), the parent ones. (b) Resolve c (x) and c (x): (i) If there is P(x) in c (x) and ? P(x) in c (x), the resolvent will be the disjunction of c (x) and c (x) with P(x) and ? P(x) disappeared. i j j i j i i j (ii) If there is a pair of literals L (x) and ? L (x) such that one of the parent clause contains L (x) and the other contains ?L (x), and if L (x) and L (x) are unifiable, then by using unification make them identical, and the resolvent will be the disjunction of c (x) and c (x) with appropriate substitution performed and with L (x) and L (x) disappeared. (c) If the resolvent is NIL, a contradiction is found。 R) 7. ? D(A) {A/z} (6, 2。 R) MORTAL(S) ? MAN(S) MAN(S) NIL Refutation Tree ?MAN(x) ? MORTAL (x) {S/x} Example 3 Theorem: The inner alternate angles of a trapezoid are equal. Symbols: 1. T(x,y,u,v) denotes a trapezoid: xyuv 2. P(x,y,u,v): xy//uv 3. E(x,y,v,u,v,y): ∠ xyv = ∠ uvy a (x) b (y) c (u) d (v) S: Premises 1. (?x)(?y)(?u)(?v) (T(x,y,u,v) ? P(x,y,u,v)) 2. (?x)(?y)(?u)(?v) (P(x,y,u,v) ? E(x,y,v,u,v,y)) 3. T(a,b,c,d) G: Theorem 4. E(a,b,d,c,d,b) Proof: 1. ?T(x,y,u,v) ? P(x,y,u,v) (Premise) 2. ? P(x,y,u,v) ? E(x,y,v,u,v,y) (Premise) 3. T(a,b,c,d) (Premise) 4. ?E(a,b,d,c,d,b) (Negated Conclusion) 5. ?P(a,b,c,d) {a/x, b/y, c/u, d/v} (2,4) 6. ?T(a,b,c,d) {a/x, b/y, c/u, d/v} (1,5) 7. NIL (3,6) a b c d 6. Answer Extraction System A Modified Version Example: S: If Fido goes wherever John goes (?x) (AT(J, x) ? AT(F, x)) and if John is at School. AT(J, S) G: Where is Fido? (?x) (AT(F, x)) ?AT(F, x) ?AT(J, y)?AT(F, y) ?AT(J, x) AT(J, S) NIL {x/y} {S/y} A Refutation Tree Approach: ?G A Proof Tree Approach ?AT(F, x) ? AT(F, x) ? AT(J, y) ? AT(F, y) AT(J, S) AT(F, S) {x/y} ? AT(J, x) ? AT(F, y) {S/x} ? G ? G The Answer Chapter 5 Information Processing amp。 Skolemize。 * Any remaining variables are assumed to have universal quantification. Example: Given a wff below: (?u) (?v) {Q(v,u) ??[[R(v)? P(v)] ?S(u,v)]} (?u) (?v) {Q(v,u) ? [[?R(v) ? ?P(v)] ? ?S(u,v)]}