(A1) "Every house is owned by a manager or a NBA-player." (A2) "Every manager owns at least one house." (A3) "All house-owners are rich." |- (A) " All managers are rich." (B) "Some NBA-player are rich." Representation of (A1), (A2), (A3), ~(A), and ~(B) in predicate calculus: (A1) Vh Vo ((house(h) ^ owns(o,h)) --> (nba(o) v manager(o) )) (A2) Vm (manager(m) --> ]h (house(h) ^ owns(m,h) )) (A3) VxVy ((owns(x,y) ^ house(y) ) --> rich(x) ) ~(A) ~Vz (manager(z) --> rich(z) ) ~(B) ~]u (nba(u) ^ rich(u)) Transformation of the above expressions to clause-form: notations: a) Capital letters represent Skolem functions b) Identifiers beginning with \$ represent variables c) All other identifiers represent constants (C1) ~house(\$h) v ~owns(\$o,\$h) v nba(\$o) v manager(\$o) (C2a) ~manager(\$m) v house(F(\$m)) (C2b) ~manager(\$m) v owns(m,F(\$m)) (C3) ~owns(\$x,\$y) v ~house(\$y) v rich(\$x) (C4a) manager(Z) (C4b) ~rich(Z) (C5) ~nba(\$u) v ~rich(\$u) Try to prove: a) A1,A2,A3 |- A (A6) house(F(Z)) from (C4a) and (C2a) (A7) owns(Z,F(Z)) " (C4a) and (C2b) (A8) ~owns(Z,\$y) v ~house(\$y) from (C4b) and (C3) (A9) ~house(F(Z)) from (A8) and (A9) (A10) empty clause from (A6) and (A9) that is, a prove for A1,A2,A3 |- A has been found Try to prove: b) A1,A2.A3 |- B (B6) ~rich(\$u) v manager(\$u) v ~owns(\$u,\$h) v ~house(\$h) from (C5) and (C1) (B7) manager(\$u) v ~owns(\$u,\$h) v ~house(\$h) v ~owns(\$u,\$y) v ~house(\$y) from (B7) and (C3). Assuming \$h is bound to \$y, (B7) can be simplified yielding: (B7') manager(\$u) v ~owns(\$u,\$y) v ~house(\$y) that is, "every house owner is a manager". However, although further resolution steps are applicable, the above formula cannot be fal- sified; that is A1,A2,A3 |- B cannot be proved. If "all house owners are managers" holds A1,A2,A3 are true, although B is not true because in this case no house is owned by an NBA-player. (A1) "Some dolphins eat fish." (A2) "No vegetarian eats fish." (A3) "Every dolphin is intelligent." (A4) "The dolphin 'Flipper' is a vegetarian." (A) "Some intelligent beings are vegetarians." (B) "Flipper is intelligent." (C) "All fish eaters are intelligent." (D) "Some dolphins are no vegetarians" (A1) ]x (dolphin(x) ^ eatfish(x) ) (A2) ~]v (vegetarian(v) ^ eatfish(v) ) (A3) Vd (dolphin(d) --> intelligent(d) ) (A4) dolphin(Flipper) ^ vegetarian(Flipper) (~A) ~]i (intelligent(i) ^ vegetarian(i)) (~B) ~intelligent(Flipper) (~C) ~Ve (eatfish(e) --> intelligent(e) ) (~D) ~]a (dolphin(a) ^ ~vegetarian(a)) (1a) dolphin(D) (1b) eatfish(D) (2) ~vegetarian(\$v) v ~eatfish(\$v) (3) ~dolphin(\$d) v intelligent(\$d) (4a) dolphin(Flipper) (4b) vegetarian(Flipper) (5) ~intelligent(\$i) v ~vegetarian(\$i) (6) ~intelligent(Flipper) (7a) eatfish(E) (7b) ~intelligent(E) (8) ~dolphin(\$a) v vegetarian(\$a) A1,A2,A3 |- A (x1) ~dolphin(\$d) v ~vegetarian(\$d) from (5) and (3) (x2) ~vegetarian(Flipper) from (x1) and (4a) (x3) empty clause from (x2) and (4b) A1,A2,A3 |- B (y1) ~dolphin(Flipper) from (6) and (3) (y2) empty clause from (y1) and (4a) A1,A2,A3 |- C (z1) ~vegetarian(E) from (7a) and (2) (z2) ~dolphin(E) from (7b) and (3) ... (no proof found). A1,A2,A3 |- D (w1) ~eatfish(\$v) v ~dolphin(\$v) from (2) and (8) (w2) ~eatfish(D) from (w1) and (1a) (w3) empty clause from (w2) and (1b) (A1) "If someone is not rich, then he is not married." (A2) "Everyone, who is rich, is not married." (A3) "If x is married to y, then y is married to x." (A) "No rich person is married to a poor(non rich) person." (A1) Vp (~rich(p) --> ]m married(p,m) ) (A2) Vz (rich(z) --> ~]w married(z,w) ) (A3) VuVv (married(u,v) --> married(v,u) ) (~A) ~~ ]x]y (rich(x) ^ ~rich(y) ^ married(x,y) ) (1) rich(\$p) v married(\$p,F(\$p)) (2) ~rich(\$z) v ~married(\$z,\$w) (3) ~married(\$u,\$v) v married(\$v,\$u) (4a) rich(X) (4b) ~rich(Y) (4c) married(X,Y) proof: A1,A2,A3 |- A (q1) ~married(X,\$w) from (4a) and (2) (q2) married(Y,F(Y)) from (4b) and (1) (q3) ~rich(X) from (4c) and (2) (q4) empty clause from (q3) and (4a) remark: Resolving (q1) and (4c) also generates the empty clause. Tranforming predicate calculus to clauses 1) Replace --> using: (P --> Q) = (~P v Q) 2) Move ~ inside using: 1) ~Vx Px = ]x ~Px 2) ~]x Qx = Vx ~Qx 3) ~(P ^ Q) = ~P v ~Q 4) ~(P v Q) = ~P ^ ~Q 3) Standardize variables - rename variables that are used more than once by quantifiers. 4) remove ]; replace existential quantified variables by Skolem functions. Use different functions for different variables; use capital letters for function names; the arity of the Skolem function is determined by the number of V-quantifiers enclosing the ]-quantifier. 5+6) remove V; replace all quantified variables by match variables. 7) Produce CNF using the Distributive law for v and ^ moving v inside and ^ outside, for example: (P ^ Q) v (R ^ S) = (P v R) ^ (P v S) ^ (Q v R) ^ (Q v S) 8) Remove ^; produce clauses. 9) Rename match variables that occur more than once in clauses.