-------------------------------------------------------------------------------------------------- Logic in Computer Science, January 11st, 2024. Time: 2h30min. No books or lecture notes allowed. -------------------------------------------------------------------------------------------------- Note on evaluation: eval(propositional logic) = max(eval(Problems 1,2,3), eval(midterm exam)) eval(first-order logic) = eval(Problems 4,5,6). - Insert your answers on the dotted lines ... below, and only there. - Do NOT modify the problems - When finished, upload this file with the same name: exam.txt - Use the text symbols: & v - -> |= A E === for AND OR NOT IMPLIES "SATISFIES" FORALL EXISTS LOGICAL EQUIV. like in: I |= p & (q v -r) ( the interpretation I satisfies the formula p & (q v -r) ). You can write subindices using "_". For example write x_i to denote x-sub-i. -------------------------------------------------------------------------------------------------- Problem 1. (3 points). 1a) For each one of the following statements, indicate if it is true or false for propositional logic. Answer T (true) or F (false) on each dotted line ... Give no explanations why. Below always F,G,H are formulas and I is an interpretation. Note: Wrong answers subtract 0.2 points. Unanswered questions subtract 0.1 points. 1) ... It is decidable in polynomial time whether a given formula in DNF is satisfiable. 2) ... Given a set of Horn clauses S, we can find in linear time a minimal model I of S, that is, a model I with the minimal |{ p | I(p)=1 }|. 3) ... If F is unsatisfiable, then -F |= F. 4) ... Given a formula F, the Tseitin transformation of F is a set of clauses that is logically equivalent to F. 5) ... The closure under resolution Res(S) of a finite set of clauses S is always a finite set of clauses. 6) ... There are formulas F and G such that F |= G and F |= -G. 7) ... There are infinitely many different formulas, even if there is only one predicate symbol. 8) ... F is satisfiable if, and only if, all logical consequences of F are satisfiable formulas. 9) ... There are infinitely many different formulas that are not logically equivalent, even if there is only one predicate symbol. 10) ... Given I and F, it is decidable in linear time whether I |= F. 11) ... Given a formula F, the Tseitin transformation of F always has a number of clauses that is linear in the size of F. 12) ... The closure under resolution Res(S) of a finite set of clauses S is always a DNF. Answer: 1) T It is decidable in polynomial time whether a given formula in DNF is satisfiable. 2) T Given a set of Horn clauses S, we can find in linear time a minimal model I of S, that is, a model I with the minimal |{ p | I(p)=1 }|. 3) F If F is unsatisfiable, then -F |= F. 4) F Given a formula F, the Tseitin transformation of F is a set of clauses that is logically equivalent to F. 5) T The closure under resolution Res(S) of a finite set of clauses S is always a finite set of clauses. 6) T There are formulas F and G such that F |= G and F |= -G. 7) T There are infinitely many different formulas, even if there is only one predicate symbol. 8) T F is satisfiable if, and only if, all logical consequences of F are satisfiable formulas. 9) F There are infinitely many different formulas that are not logically equivalent, even if there is only one predicate symbol. 10) T Given I and F, it is decidable in linear time whether I |= F. 11) T Given a formula F, the Tseitin transformation of F always has a number of clauses that is linear in the size of F. 12) F The closure under resolution Res(S) of a finite set of clauses S is always a DNF. 1b) You have three closed boxes in front of you, two of them empty and one full of gold. The lid of each box contains a statement regarding its contents. Box A says "The gold is not here", box B says "The gold is not here" and box C says "The gold is in box B." If we know that one and only one statement is true, which box contains the gold? Define the necessary predicate symbols, formalize the statements, and decide which is the correct interpretation. Answer: ... a means: "The gold is in box A" b means: "The gold is in box B" c means: "The gold is in box C" (unnecessary) box A says: -a box B says: -b box C says: b Let's see which interpretation meets the requirements that: - exactly one and only one of the statements is true, and - the gold is only in one of the boxes I(a) = 1, I(b) = 1, then the requirement that the gold is only in one of the boxes is not met. I(a) = 0, I(b) = 0, then two of the statements are true, which is not allowed I(a) = 0, I(b) = 1, then two of the statements are true, which is not allowed I(a) = 1, I(b) = 0, satisfies all requirements Therefore the gold is in box A. -------------------------------------------------------------------------------------------------- Problem 2. (4 points). 2a) Let F and G be two formulas. Prove that F |= G if and only if F & -G is unsatisfiable. Prove it as simply as you can using only the definitions of propositional logic, filling the dots ... below (use as many lines as you need). F |= G iff [ by def. of logical consequence ] A I, I |= F implies I |= G iff [ by def. of implies ] A I, I \|= F or I |= G ... ... Answer: F |= G iff [ by def. of logical consequence ] A I, I |= F implies I |= G iff [ by def. of implies ] A I, I \|= F or I |= G iff [ by def. of |= ] A I, eval_I(F) = 0 or eval_I(G) = 1 iff [ by arithmetic ] A I, eval_I(F) = 0 or 1-eval_I(G) = 0 iff [ by def eval_I( - ) ] A I, eval_I(F) = 0 or eval_I(-G) = 0 iff [ by def. of min ] A I, min(eval_I(F), eval_I(-G)) = 0 iff [ by def. of eval_I( & ) ] A I, eval_I(F & -G) = 0 iff [ by def. of |= ] A I, I \|= F & -G iff [ by def. of unsatisfiable ] F & -G is unsatisfiable 2b) Let F be a formula. Prove that the formulas F and --F (double negation) are logically equivalent: Prove it as simply as you can using only the definitions of propositional logic, filling the dots ... below (use as many lines as you need). F === --F iff [ by def. of logical equivalence ] A I, I |= F if and only if I |= --F iff [ by def. of if and only if, and |= ] A I, eval_I(F) = eval_I(--F) ... ... Answer: F === --F iff [ by def. of logical equivalence ] A I, I |= F if and only if I |= --F iff [ by def. of if and only if, and |= ] A I, eval_I(F) = eval_I(--F) iff [ by def. of eval_I( - ) ] A I, eval_I(F) = 1-eval_I(-F) iff [ by def. of eval_I( - ) ] A I, eval_I(F) = 1-(1-eval_I(F)) iff [ by arithmetic ] A I, eval_I(F) = eval_I(F) iff [ ] true 2c) Let F,G,H be three formulas. Prove that F & G |= H if and only if F |= G -> H Prove it as simply as you can using the definitions of propositional logic, but in THIS section you can use (as a step of the proof) the following: * the result of exercise 2a): F1 |= F2 iff F1 & -F2 is unsatisfiable * the result of exercise 2b) -double negation-: --F1 === F1 * the logical equivalence of associativity of &: (F1 & F2) & F3 === F1 & (F2 & F3) * the Substitution lemma * the logical equivalence of De Morgan law of &: -(F1 & F2) === (-F1 v -F2) F & G |= H iff [ by exercise 2a) ] (F & G) & -H is unsatisfiable ... ... Answer: F & G |= H iff [ by exercise 2a) ] (F & G) & -H is unsatisfiable iff [ by associativity of & ] F & (G & -H) is unsatisfiable iff [ by exercise 2b), and Substitution lemma ] F & --(G & -H) is unsatisfiable iff [ by De Morgan, and Substitution lemma ] F & -(-G v --H) is unsatisfiable iff [ by exercise 2b), and Substitution lemma ] F & -(-G v H) is unsatisfiable iff [ by exercise 2a) ] F |= -G v H) iff [ by definition of -> ] F |= G -> H -------------------------------------------------------------------------------------------------- Problem 3. (3 points). Consider the following particular case of the resolution ("unitary" resolution): p -p ∨ C -------------- C where p is a propositional symbol. 3a) Prove that the unitary resolution is correct. Answer: ... It is correct if whatever p and C, we have that p & (-p v C) |= C Let I be a model of p & (-p v C) For p there is only one choice: I(p) = 1 And then: I |= p & (-p v C) ==> I |= -p v C ==> I |= C So unitary resolution is a *correct* deductive rule in LProp. 3b) Prove that the "unitary" resolution is not refutationally complete for clauses that are not Horn. Answer: ... Counterexample: C1: p v q C2: -p C3: -q This set of non-Horn clauses is unsatisfiable, but the empty clause cannot be generated by "unitary" resolution, so unitary resolution is not refutationally complete for clauses that are not Horn. -------------------------------------------------------------------------------------------------- _____________________________________________________________________________________ _____________________________________________________________________________________ FIRST-ORDER LOGIC: _____________________________________________________________________________________ _____________________________________________________________________________________ Problem 4. (4 points). 4a) Let F and G be two FOL formulas. The formulas Ex (F -> G) and Ex F -> Ex G are logically equivalent? Answer: ... It is false. Counter example: Let F = p(x), G = q(x), and consider the following interpretation I: D_I = {a,b} p_I(a) = 1 p_I(b) = 0 q_I(a) = q_I(b) = 0 We have I |= Ex (F -> G) but I \|= Ex F -> Ex G Therefore, the formulas Ex (F -> G) and Ex F -> Ex G are not logically equivalent. 4b) Prove that resolution without factorization in FOL is not refutationally complete. Hint: give a counterexample of two clauses with two literals each. Answer: ... S = { p(x) v p(y), -p(z) v -p(z') } In the clauses of this set S, literals do not share variables. The only thing I can get through resolution is other clauses where literals do not share variables either. For example: p(x) v p(y) -p(z) v -p(z') --------------------------------------- with mgu(p(x),p(z)) = {x=z} p(y) v -p(z') And so, in this example, I'm always going to keep getting clauses of two literals! And the empty clause will never come out. 4c) Write a formula F in FOLE that expresses that for every model I of F there are at most n elements in the domain of I, for a given natural n Answer: ... a) a quadratic size formula: Ax_1 ... Ax_{n+1} ( V 1<=i Ey ( -(x=y) & f(x,x)=f(y,y) ) ) or with != Ax ( Ez f(x,z)!=x --> Ey ( x!=y & f(x,x)=f(y,y) ) ) ------------------------------------------------------------------------------------ Problem 6. (3 points). "The footbridge over the river" A sign at the beginning of the footbridge states the following: A. The passage of more than one person is not allowed simultaneously on the footbridge. B. If x and y are the same person and x is adult, then y is adult C. Minors will be accompanied by an adult. Prove in **FOL** that: D. Minors cannot cross the footbridge. Use these predicats: p(x): "x pass through the footbridge" a(x): "x is adult" e(x,y): "x and y are the same person" Answers (after every "..."): A. The passage of more than one person is not allowed simultaneously on the footbridge ... Ax Ay ( (p(x) & p(y)) -> e(x,y) ) definition of -> Ax Ay (-p(x) v -p(y) v e(x,y)) A. -p(x) v -p(y) v e(x,y) B. If x and y are the same person and x is adult, then y is adult ... Ax Ay ( (e(x,y) & a(x)) -> a(y) ) definition of -> Ax Ay (-e(x,y) v -a(x) v a(y)) B. -e(x,y) v -a(x) v a(y) C. Minors will be accompanied by an adult. ... Ax ( (p(x) & -a(x)) -> Ey (p(y) & a(y)) ) definition of -> Ax ( -p(x) v a(x) v Ey (p(y) & a(y)) ) Skolemization: Ax ( -p(x) v a(x) v (p(f_y(x)) & a(f_y(x))) ) distributivity: Ax ( (-p(x) v a(x) v p(f_y(x))) & (-p(x) v a(x) v a(f_y(x))) ) C1. -p(x) v a(x) v p(f_y(x)) C2. -p(x) v a(x) v a(f_y(x)) D. Minors cannot cross the footbridge. ... Ax ( -a(x) -> -p(x) ) definition of -> Ax ( a(x) v -p(x) ) the negation: -D. ... -D. - ( Ax ( a(x) v -p(x) ) ) moving - inside: Ex ( -(a(x) v -p(x)) ) De Morgan: Ex ( -a(x) & p(x) ) Skolemization (c_x is a constant): -a(c_x) & p(c_x) -D1. -a(c_x) -D2. p(c_x) We have to see that the set of clauses: A. ... B. ... ... A. -p(x1) v -p(y1) v e(x1,y1) B. -e(x2,y2) v -a(x2) v a(y2) C1. -p(x3) v a(x3) v p(f_y(x3)) C2. -p(x4) v a(x4) v a(f_y(x4)) -D1. -a(c_x) -D2. p(c_x) is unsatisfiable Applying resolution: 1. ... + ... ... with mgu(..., ...) = {...} 2. ... + ... ... with mgu(..., ...) = {...} ... 1. C1 + -D1 -p(c_x) v p(f_y(c_x)) with mgu(a(x3), a(c_x)) = {x3=c_x} 2. C2 + -D1 -p(c_x) v a(f_y(c_x)) with mgu(a(x4), a(c_x)) = {x4=c_x} 3. -D2 + 1 p(f_y(c_x)) with mgu = { } 4. -D2 + 2 a(f_y(c_x)) with mgu = { } 5. 3 + A -p(y) v e(f_y(c_x), y) with mgu(p(x1), p(f_y(c_x))) = {x1=f_y(c_x)} 6. -D2 + 5 e(f_y(c_x), c_x) with mgu(p(c_x), p(y1)) = {y1=c_x} 7. 6 + B -a(f_y(c_x)) v a(c_x) with mgu(e(f_y(c_x),c_x), e(x2,y2)) = {x2=f_y(c_x), y2=c_x} 8. 4 + 7 a(c_x) with mgu = { } 9. 8 + -D1 [] with mgu = { } In more detail: 1. C1 + -D1 -p(c_x) v p(f_y(c_x)) with mgu(a(x3), a(c_x)) = {x3=c_x} C1. -p(x3) v a(x3) v p(f_y(x3)) -D1. -a(c_x) ---------------------------------------------------------- with mgu(a(x3), a(c_x)) = {x3=c_x} 1. -p(c_x) v p(f_y(c_x)) 2. C2 + -D1 -p(c_x) v a(f_y(c_x)) with mgu(a(x4), a(c_x)) = {x4=c_x} C2. -p(x4) v a(x4) v a(f_y(x4)) -D1. -a(c_x) ---------------------------------------------------------- with mgu(a(x4), a(c_x)) = {x4=c_x} 2. -p(c_x) v a(f_y(c_x)) 3. -D2 + 1 p(f_y(c_x)) with mgu = { } -D2. p(c_x) 1. -p(c_x) v p(f_y(c_x)) ---------------------------------------------------------- with mgu = { } 3. p(f_y(c_x)) 4. -D2 + 2 a(f_y(c_x)) with mgu = { } -D2. p(c_x) 2. -p(c_x) v a(f_y(c_x)) ---------------------------------------------------------- with mgu = { } 4. a(f_y(c_x)) 5. 3 + A -p(y) v e(f_y(c_x), y) with mgu(p(x1), p(f_y(c_x)))= {x1=f_y(c_x)} 3. p(f_y(c_x)) A. -p(x1) v -p(y1) v e(x1,y1) ---------------------------------------------------------- with mgu(p(x1), p(f_y(c_x)))= {x1=f_y(c_x)} 5. -p(y1) v e(f_y(c_x), y1) 6. -D2 + 5 e(f_y(c_x), c_x) with mgu(p(c_x), p(y1)) = {y1=c_x} -D2. p(c_x) 5. -p(y1) v e(f_y(c_x), y1) ---------------------------------------------------------- with mgu(p(c_x), p(y1)) = {y1=c_x} 6. e(f_y(c_x), c_x) 7. 6 + B -a(f_y(c_x)) v a(c_x) with mgu(e(f_y(c_x),c_x), e(x2,y2)) = {x2=f_y(c_x), y2=c_x} 6. e(f_y(c_x), c_x) B. -e(x2,y2) v -a(x2) v a(y2) ---------------------------------------------------------- with mgu(e(f_y(c_x),c_x), e(x2,y2)) = {x2=f_y(c_x), y2=c_x} 7. -a(f_y(c_x)) v a(c_x) 8. 4 + 7 a(c_x) with mgu = { } 4. a(f_y(c_x)) 7. -a(f_y(c_x)) v a(c_x) ---------------------------------------------------------- with mgu = { } 8. a(c_x) 9. 8 + -D1 [] with mgu = { } 8. a(c_x) -D1. -a(c_x) ---------------------------------------------------------- with mgu = { } 9. [] ------------------------------------------------------------------------------------