Report

Lesson 9 Resolution method (continuing, examples) 1 Verifying an argument: (Anybody) who knows Paul and Mary is sorry for Mary. Some are not sorry for Mary, though they know her. ––––––––––––––––––––––––––––––– Somebody knows Mary, but does not know Paul. x [Z(x, P) Z(x, M) L(x, M)] L(a, M) Z(a, M) y [Z(y, M) Z(y, P)] Clauses: 1. 2. 3. 4. 5. 6. 7. 8. Z(x, P) Z(x, M) L(x, M) L(a, M) Z(a, M) Z(y, M) Z(y, P) Z(a, P) Z(a, M) Z(a, P) Z(a, M) x ( [Z(x, P) Z(x, M)] L(x, M) ) x [L(x, M) Z(x, M)] x [Z(x, M) Z(x, P)] implication elimination (1. assumption) „Scolemising“ (2. assumption) negation of conclusion (and renaming x) (2. assumption is a conjunction: two clauses arise!) resolution 1., 2., substitution a/x resolution 3., 5. resolution 4., 6., substitution a/y resolution 3., 7. We obtained an empty clause, i.e., the negated conclusion contradicts the premises; thus the non-negated original conclusion logically follows from the premises. The argument is valid. 2 Remark: Compare the proof of this argument with the semantic proof (lesson 6, slides 22, 23) We demonstrate the truth-conditions of the premises first; the predicates Z and L are interpreted as the relations ZU and LU, respectively: ZU = {…, i1,m, i1,k, i2,m, i2,k,…,,m,… } 1. premise 2. premise LU = {…, i1,m, ...., i2,m,…........., ,m,… } and so on, by the method of an indirect proof 3 Indirect proof of the validity of an argument We make use of the following equivalence valid for closed formulas: P1,...,Pn |= Z iff |= (P1 ... Pn) Z Moreover |= (P1 ... Pn) Z iff the negated formula is a contradiction: (P1 ... Pn Z) Hence, the argument is valid iff the negated conclusion Z contradicts the conjunction of premises. Indeed, compare with the definition of the validity of an argument: P1,...,Pn |= Z iff Z is true in every model of the set of premises P1,...,Pn iff Z is true in no model of the set of premises. 4 Proofs of the validity: Prove, that the following statement „If there is a philosopher who disagrees with all the philosophers, then he disagrees with himself as well“ is logically true. We analyse this sentence in following way: (”intended” interpretation is over the set of individuals, P subset of philosophers, Q relation: the couples of individuals where the first member disagrees with the second) We prove the logical validity of the formula: x {[P(x) y (P(y) Q(x,y))] Q(x,x)} First, negate the formula and transform it into clausul form: x y {P(x) [P(y) Q(x,y)] Q(x,x)}. The set of clauses: 1. P(x) 2. P(y) Q(x,y) 3. Q(x,x) the substitution {y/x} is the most general unifier: 4. Q(x,x) 5. resolution 1. and 2. resolution 3. and 4. 5 Proofs of the validity: Prove the logical validity of following statement: Formula: x [G(x) x G(x)] (mind the brackets!) We prove, that the negated formula is a contradiction: 1. 2. 3. „There is somebody such that if he\she is a genius, then everybody is a genius“. x [G(x) x G(x)], renaming variables gives: x [G(x) y G(y)], step 6: [x G(x) y G(y)] and by Scolemizing we have: x [G(x) G(a)]. G(x) G(a) resolution 1. and 2., substitution a/x We obtained an empty clause, i.e., the negated formula is a contradiction; so the original formula is a tautology. 6 Every member of the management is an obligation owner or a shareholder. 2. No member of the management is an obligation owner and also a shareholder. 3. Every obligation owner is a member of the management. –––––––––––––––––––––––––––––––––––––––––––––––– 4. No obligation owner is a shareholder. 1. x [V(x) (O(x) A(x))] x [V(x) (O(x) A(x))] x [O(x) V(x)] ––––––––––––––––––––– x [O(x) A(x)] Clauses: 1. 2. 3. 4. 5. 6. 7. 8. V(x) O(x) A(x) V(y) O(y) A(y) O(z) V(z) O(k) A(k) O(y) A(y) A(k) 1. premise 2. premise 3. premise negated conclusion (after Scolemization) resolution 2., 3., substitution z/y resolution 4., 6., substitution y/k resolution 5., 7. Note that we do not use the first clause in the proof sequence. So conclusion is a consequent of the second and the third premise (the first one is superfluous for infering the conclusion). 7 Everybody who likes George will collaborate with Michael. Michael is a friend of nobody who is a friend of Luke. Peter will collaborate only with the friends of Charles. –––––––––––––––––––––––––––––––––––––––––––––– If Charles is a friend of Luke, then Peter does not like George. x [L(x, G) C(x, M)] x [F(x, L) F(M, x)] x [C(P, x) F(x, Cr) –––––––––––––––––––– F(Cr, L) L(P, G) Clauses: 1. L(x, G) C(x, M) 2. F(y, L) F(M, y) 3. C(P, z) F(z, Cr) 4. F(Cr, L) 5. L(P, G) 6. F(M, Cr) 7. C(P, M) 8. L(P, G) 9. 1. premise 2. premise 3. premise negated conclusion resolution 4., 2., substitution y/Cr resolution 3., 6., substitution z/M resolution 1., 7., substitution x/P resolution 5., 8. 8 What are the logical consequences of premises? Variant of the preceding example. Premises do not contain existential statement. Everybody who likes George will collaborate with Michael. Michael is a friend of nobody who is a friend of Luke. Peter will collaborate only with the friends of Charles. Charles is a friend of Luke. –––––––––––––––––––––––––––––––––––––––––––––– ??? Clauses: 1. L(x, G) C(x, M) 2. F(y, L) F(M, y) 3. C(P, z) F(z, Cr) 4. F(Cr, L) 5. F(M, Cr) 6. L(P, G) F(M, Cr) 7. L(P, G) 8. C(P, M) 1. premise 2. premise 3. premise 4. premise inference, resolution 2,4, y/Cr inference, resolution 1,3, x/P, z/M inference, resolution 5,6 inference, resolution 3,5, z/M 9 Indirect proof of the validity of an argument All men like football and beer. Xaver likes only those who like football and beer. There is somebody who likes football but does not like beer. Anybody who is not a man is a woman. (we must not omit tacit premises) ––––––––––––––––––––––––––––––––––––– Some women are not liked by Xaver. x [M(x) (R(x,f) R(x,p))] x [R(Xa,x) (R(x,f) R(x,p))] x [R(x,f) R(x,p)] x [M(x) Z(x)] x [Z(x) R(Xa,x)] 1. premise 2. premise 3. premise 4. premise negated conclusion 10 Indirect proof of the argument Clauses: 1. M(x) R(x,f) 2. M(x) R(x,p) 3. R(Xa,y) R(y,f) 4. R(Xa,y) R(y,p) 5. R(k,f) 6. R(k,p) 7. M(z) Z(z) 8. Z(u) R(Xa,u) ––––––––––––––––––– 9. R(Xa,k) 10. Z(k) 11. M(k) 12. R(k,p) 13. first premise second premise third premise after Scolemization: x/k 4. premise negated conclusion resolution 4., 6. (y/k) resolution 8., 9. (u/k) resolution 7., 10. (z/k) resolution 2., 11. (x/k) resolution 6., 12. We have found out again that the negated conclusion contradicts the premises, so that the argument is valid. Do you know which premises were not necessary for inferring the conclusion? 11 Proof by the resolution method |= If a number is even then its second power is even . If a number is even then its fourth power is even . |= y [P(y) Pf(y)] x [P(x) P(f(f(x)))] – negate it: x [P(x) P(f(f(x)))] – Scolemise: [P(a) P(f(f(a)))] – write down the clauses: 1. 2. 3. 4. 5. 6. P(y) Pf(y) P(a) P(f(f(a))) P(f(a)) P(f(f(a))) premise negated conclusion resolution 1-2, substitution y/a resolution 1-4, substitution y/f(a) resolution 3-5, contradiction The argument is valid. 12 Mathematical induction P(a), y [P(y) Pf(y)] | x P(x) Is the derived formula a logicall consequence of the premises? In other words, is the mathematical-induction rule correct, i.e., does it preserve truth? Clauses: 1. P(a) 2. P(y) P(f(y)) 3. P(f(a)) inference 2.1., subst. y/a 4. P(f(f(a))) inference 2.3., subst. y/f(a) 5. P(f(f(f(a))))inference 2.4., subst. y/f(f(a)) 6. and so on, ad infinitum. We cannot prove it by the indirect proof as well, because the negated conclusion is (after scolemising): P(b) and the terms b, a, f(a), f(f(a)),… are not unifiable. We never prove that x P(x) – the case of the actual infinity. We can only reach the potential infinity … potentially we can go ad infinitum; but not really. 13 Verifying the consistence There is a barber who shaves just all those who do not shave themselves. Does this barber shave himself? x y [H(y,y) H(x,y)] |= ? H(x,x) In Lesson 7 we have seen that the premise is a contradiction; so such a barber does not exist. We prove it by the resolution method. We add the negated conclusion to the premise and write down the clauses. x y [H(y,y) H(x,y)] |= ? H(x,x) 1. H(y,y) H(a,y) H(a,a) substitution y/a 2. H(y,y) H(a,y) H(a,a) substitution y/a 3. H(x,x) 4. resolution 1., 2., substitution y/a We don´t need the third clause (negated conclusion) in order to infer the contradiction. So the premise is contradictory. Such a barber does not exist. 14 Note: Robinson‘s algorithm of the general resolution and unification operates also on particular literals of a clause. For instance, from the clauses 1. P(x,y) Q(a,f(y)) P(x,a) Q(y,x) P(f(a),a) Q(a,f(a)) 2. P(f(z),z) P(v,a) P(f(a),a) we derive the resolvent Q(a,f(a)), after the unification x/f(a), y/a, z/a, v/f(a), because the first clause is unified into P(f(a),a) Q(a,f(a)) and the second into P(f(a),a). Note: Pay attention to equivalences Formula A B is not contradictory, it is satisfiable b) Formula A A is contradictory Clauses ad a) 1. A B 2. A B now in each step we can generate the resolvent by the resolution of only one pair of literals, so no empty clause is derived: 3. B B 4. A A Clauses ad b) 1. A A A 2. AA A 3. 1. and 2. resolve into the empty clause a) 16 Checking the consistence Mr X changed his job and got a more qualified one (K). Mr X knows the wage-payment system very well (M). If Mr X changed his job for the more qualified one, then it is right to discuss his case (P). If is it right to discuss his case, then he should not be a member of the commission (C). If he knows the wage-payment system very well, then he should be a member of the commission. What are the logical consequences? We check the consistence of the set of statements first. K M (K P) (P C) (M C) 1. K 2. M 3. K P 4. P C 5. M C 6. P resolution 1, 3 7. C resolution 4, 6 8. C resolution 2, 5 9. contradiction resolution 7, 8 The given set of statements is contradictory; so anything follows. 17 Checking the validness of a formula |=? x [P(x) y x (Q(x,y) z R(a,x,y))] z [(P(b) Q(f(z), z)) R(a, f(b), z)] We transform the antecedent to the clause form : a) By the method of Skolem algorithm b) We transform it to the prenex form at first and then we scolemise it. 18 Checking the validness of a formula vs step 6 Antecedent – transformation to the clause form, procedure a) x [P(x) y x (Q(x,y) z R(a,x,y))] Steps 2., 5. Renaming variable x and eliminating z: x [P(x) y u (Q(u,y) R(a,u,y))] Step 3. Elimination of the implication: x [P(x) y u (Q(u,y) R(a,u,y))] Step 6. Moving the quantifier x to the left: x P(x) y u (Q(u,y) R(a,u,y)) Step 7. Skolemization (i.e., substituting g(y) for the varible u: the symbol f is used in the conclusion, so we have to use a new one): x P(x) y (Q(g(y), y) R(a, g(y), y)) Step 8. moving the quantifier to the left: SK1: x y [P(x) (Q(g(y), y) R(a, g(y), y))]. 19 Checking the validness of a formula vs step 6 Antecedent – transformation to the clause form, procedure b) without step 6 x [P(x) y x (Q(x,y) z R(a,x,y))] Steps 2,5: Renaming variable x and eliminating z: x [P(x) y u (Q(u,y) R(a,u,y))] Step 3. Elimination of the implication: x [P(x) y u (Q(u,y) R(a,u,y))] Step 7. Skolemization (i.e., substituting g(x,y), for the varible u, because the variable u is at the scope of x): x [P(x) y (Q(g(x,y), y) R(a, g(x,y), y)) Step 8. removing the quantifier to the left: SK2: x y [P(x) (Q(g(x,y), y) R(a, g(x,y), y))]. 20 Checking the validness of a formula vs step 6 The negated conclusion (is in the clausal form already): z [(P(b) Q(f(z), z)) R(a, f(b), z)]. We attempt to prove a contradiction with SK1 (clausal form of the antecedent) We write the clauses down, procedure a): 1. P(x) premise 2. Q(g(y), y) R(a, g(y), y) premise 3. P(b) Q(f(z), z) negated conclusion 4. R(a, f(b), z) negated conclusion 5. Q(f(z), z) resolution 1., 3., substitution x / b 6. ??? We cannot derive any more resolvents, because terms g(y) a f(z), or g(y) and f(b) are not unifiable. The Formula is not a tautology. 21 Checking the validness of a formula vs step 6 We are not able to prove the contradiction with SK2 (procedure b) with the negated conclusion either : 1. P(x) 2. Q(g(x,y), y) R(a, g(x,y), y) 3. P(b) Q(f(z), z) 4. R(a, f(b), z) 5. Q(f(z), z) resolution 1., 3., substitution x / b However, we can‘t procede further, because the terms g(x,y) and f(z), possibly g(x,y) and f(b), are not unifiable. Conclusion: The Formula is not a tautology. 22 Exercise, a puzzle 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. Tom, Peter and John are members of a sport club. Every member of the club is a skier or a climber. No climber likes raining. All skiers like snow. Peter does not like what Tom likes, and does like what Tom does not like. Tom likes snow and raining. Question: Is there in the club a sportsman who is a climber but not a skier? Solution: Knowledge base (+ query 11): SC(t) SC(p) SC(j) x [ SC(x) (SKI(x) CLIMB(x)) ] x [ CLIMB(x) LIKE(x,r) ] x [ SKI(x) LIKE(x,s)] x [LIKE(t,x) LIKE(p,x)] x [LIKE(t,x) LIKE(p,x)] LIKE(t,s) LIKE(t,r) ? x [SC(x) CLIMB(x) SKI(x)] 23 Exercise, a puzzle Knowledge base (in Clausal form + negated query 11): 1. SC(t) sport-club(tom). 2. SC(p) sport-club(peter). 3. SC(j) sport-club(john). 4. SC(y) SKI(y) CLIMB(y) each club member is a skier or a climber 5. CLIMB(z) LIKE(z,r) each climber does not like raining 6. SKI(v) LIKE(v,s) each skier does not like snowing 7. LIKE(t,x1) LIKE(p,x1) Tom and Peter have opposite 8. LIKE(t,x2) LIKE(p,x2) tastes 9. LIKE(t,s) like(tom, snow). 10. LIKE(t,r) like(tom, raining). 11. SC(x) CLIMB(x) SKI(x) Query Proof by resolution that 1-11 is inconsistent. In other words, we are looking for an instantiation of the variable x, that leads to a contradiction. 12. LIKE(p,s) res.: 9, 7 by substituting s for x1 13. SKI(p) res.: 12, 6 by substituting p for v 14. SC(p) CLIMB(p) res.: 13, 4 by substituting p for y 15. CLIMB(p) res.: 14, 2 16. Resolution 11 + 2 + 13 + 15 by substituting p for x. (Obviously, the solution is p = Peter) 24 Checking the validness of an argument Situation: A couple of friends met a priest A, who said: „The first man whom I confessed was a murder“. After a while Mr B came, looked at the priest and said: „I was the first man whom the priest A confessed“. Question: Did the priest offend against the confessional secrecy? Řešení: x [(x = f(A)) V(x)] B = f(A) ??? (Intended interpretation: Let f be a function that assigns to the priest the only man confessed by the priest as the first one) Clauses: 1. (x = f(A)) M(x) 1. premise 2. B = f(A) 2. premise 3. M(B) (B is a murder) inference: resolution 1.,2., substitution x/B Solution: The priest offended against the confessional secrecy. 25 Prolog foundations (the logic) Method of („pure“) logic programming is a special case of the general resolution method. Compared to the general resolution method, it has the following restrictions: it works just with Horn‘s clauses (they have one positive literal at most), it uses the linear strategy of generating resolvents together with the process of „backtracking“ 26 Prolog foundations (the logic) In logic programming we use the following terminology: Notation: P:- Q1, Q2,..,Qn. (is equivalent to: Q1 Q2 … Qn P, or to (Q1 Q2 … Qn) P ) conditional statement (rule) Notation P. unconditional statement (fact) Notation?- Q1, Q2,..,Qn. (is equivalent to: Q1 Q2 … Qn) targets /target clauses, queries/ Notation, YES: contradiction /an empty clause / 27 Prolog foundations (the logic) Logic program is a sequence of conditional statements (rules) and unconditional statements (facts). Target clause set queries that the program tries to reply. Note: Commands are understood as being declared by stating the rules and facts. So logic programs are declarative (not imperative). We only specify ”what is to be done” and do not determine ”in which way to do it”. 28 Prolog foundations (the logic) Example: All students are younger than Peter‘s mother. Charles and Mary are students. Who is younger than Peter‘s mother? Notation in PL1: x [St(x) Mlx,matka(p)], St(k), St(m) |= ? Program in Prolog (Notice: variables - capitals, constants - small letters): younger(X, mother(peter)):- student(X). rule student(charles). fact student(mary). fact ?- younger(Y, mother(peter)). Query, target goal The interpreter performs unification and resolution following the linear strategy driven by target: a) Target ?- younger(Y, mother(peter)) is unificated with younger (X, mother(peter)), Y=X; b) New target is generated: ?- student(Y) c) This target is unificated with the 2. fact in the database: success with Y=charles d) It‘ll figure out the reply YES, Y = charles ; We can enter semicolon ‘;’ which means that we are asking „Who next?“. It envokes backtracking, i.e., the process of returning to the last target and attempting to execute it again: ?- student(Y). Now the interpreter cannot use the 2. clause again (it remembers the place that has been used already) but it can use 3. clause: e) It‘ll figure out the reply YES, Y = Mary ; NO 29 Prolog foundations (the logic) As stated above, logic programs are declarative (not imperative). We specify ”what is to be done” and do not determine ”in which way it is to be done”. The interpreter finds the way how to reply the queries, i.e., it deduces which are the logical consequences of the specified knowledge base and which values have to be substitutiated for variables by unification (answers). However, the restriction to Horn clauses can cause troubles. See the example of a puzzle (slides 19, 20) Try to formulate this puzzle in Prolog! Summary of the restrictions: one positive literal at most (no disjunction in the consequent), we are not able to specify negative facts directly. Negation as failure of inferring! 30