-------------------------------------------------------------------------------------------------- Logic in Computer Science, January 17th, 2025. 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). 1) For each one of the following statements, indicate if it is true or false for propositional logic. Answer T (true), F (false), or - (no answer) in the line *Answer1List* below. Give no explanations why. Below, always F,G and H are formulas, and I is an interpretation. *Note*: Wrong answers subtract 0.1 points. Unanswered questions subtract 0.05 points. 1) 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 }|. 2) If F is unsatisfiable, then for every G we have G |= F. 3) If S is a set of 2-SAT clauses (that is, clauses with at most two literals), then |Res(S)| is quadratic in |S|. 4) The closure under resolution Res(S) can grow infinitely, even if S is a finite set of clauses. 5) Given a formula F, the Tseitin transformation of F always has a number of clauses that is linear in the size of F. 6) The formula p & p is a logical consequence of (p v q v r) & (-q v r) & (-r). 7) It is decidable in polynomial time whether a given formula in DNF is satisfiable. 8) If there are n propositional symbols, there are 2^n (2 to the power n) different clauses. 9) F is satisfiable if, and only if, all logical consequences of F are satisfiable formulas. 10) There are formulas that are in CNF and DNF at the same time. 11) If F is a tautology, then -F is satisfiable. 12) If H is not a logical consequence of F v G, then (F v G) & -H is unsatisfiable. 13) It is decidable in polynomial time whether a given formula is a tautology. 14) For every formula F, there is a set of clauses S that is equisatisfiable to F and such that no clause in S has more than 3 literals. 15) There are known algorithms for deciding in polynomial time whether a given formula in DNF is a tautology. Answer1List( -, -, -, -, -, -, -, -, -, -, -, -, -, -, - ) 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 Answer1List( T, F, T, F, T, T, T, F, T, T, F, F, F, T, F ) -------------------------------------------------------------------------------------------------- Problem 2. (3 points). 2a) Is it true that a formula F is a tautology if, and only if, its Tseitin transformation Tseitin(F) is a tautology? Prove your answer by providing a proof a counterexample using only the definitions of propositional logic. Answer 2a: ... No. Counterexample: let F be the tautology p v -p. Tseitin(F) is a set of four clauses: { a, -a v p v -p, a v p, a v -p }. Tseitin(F) is not a tautology: not(I |= Tseitin(F)) if I(a) = 0. [Comment: Every model of F can be extended to a model of Tseitin(F) by adequately interpreting the new auxiliary variables in Tseitin(F), and, conversely, every model of Tseitin(F) can be converted into a model of F by "forgetting" about the auxiliary symbols (therefore, both are equisatisfiable: if one of them is satisfiable, the other one also is).] 2b) Let F and G denote arbitrary propositional formulas. Is -(F & -F) v G a tautology? Satisfiable? Unsatisfiable? Prove your answer by providing a proof or a counterexample using only the definitions of propositional logic. Answer 2b: ... It is a tautology, and hence it is satisfiable and not unsatisfiable. Proof: -(F & -F) v G is a tautology iff [by definition of tautology] forall I, I |= -(F & -F) v G iff [by definition of |=] forall I, eval_I( -(F & -F) v G ) = 1 iff [by definition of eval v] forall I, max( eval_I( -(F & -F) ), eval_I(G) ) = 1 iff [by definition of eval -] forall I, max( 1 - eval_I( F & -F ), eval_I(G) ) = 1 iff [by definition of eval &] forall I, max( 1 - min( eval_I( F ), eval_I(-F) ), eval_I(G) ) = 1 iff [by definition of eval -] forall I, max( 1 - min( eval_I( F ), 1-eval_I( F) ), eval_I(G) ) = 1 iff [by definition of eval ] forall I, max( 1 - 0, eval_I(G) ) = 1 iff [by arithmetic] forall I, max( 1, eval_I(G) ) = 1 iff [by definition of eval and arithmetic] 1 = 1 -------------------------------------------------------------------------------------------------- Problem 3. (4 points). 3) Let us remember the Heule-3 encoding for at-most-one (AMO) which expresses in CNF that at most one of the literals x_1 ... x_n is true, also written x_1 + ... + x_n <= 1. It uses the fact that AMO(x_1, ..., x_n) iff AMO(x_1, x_2, x_3, aux) & AMO(-aux, x_4, ..., x_n). Then, the part AMO(-aux, x_4, ..., x_n), which has n−2 variables, can be encoded recursively in the same way, and AMO(x_1, x_2, x_3, aux) can be expressed using the quadratic encoding with 6 clauses. In this way, to eliminate two variables we need one auxiliary variable and six clauses, so in total, for values of n much larger than the base case, we need approximately n/2 variables and 3n clauses. 3a) We now want to extend the encoding for at-most-two (AMT, also written x_1 + ... + x_n <= 2). Prove that AMT(x_1, ..., x_n) has a model I iff AMT(x_1, x_2, x_3, aux_1, aux_2) & AMT(-aux_1, -aux_2, x_4, ..., x_n) has a model I′, with I(x_i) = I′(x_i) for all i in 1 ... n. ==> : If I |= AMT(x_1, ..., x_n) and k is the number of literals in {x_1, x_2, x_3} that are true in I, then we extend I into I' as follows: Answer 3a1: ... - If k = 0, we set I′(aux_1) = I′(aux_2) = 1; - If k = 1, we set (for example) I′(aux_1) = 1 and I′(aux_2) = 0; - If k = 2, we set I′(aux_1) = I′(aux_2) = 0. In all three cases, I′ |= AMT(x_1, x_2, x_3, aux_1, aux_2) & AMT(-aux_1, -aux_2, x_4, ..., x_n). <== : If I′ |= AMT(x_1, x_2, x_3, aux_1, aux_2) & AMT(-aux_1, -aux_2, x_4, ..., x_n) then, Answer 3a2: ... "forgetting" the part of the auxiliary variables, in all cases the resulting I is a model of AMT(x_1, ..., x_n), because: – If I′(aux_1) = I′(aux_2) = 1 then I |= -x_1 & -x_2 & -x_3 and I |= AMT(x_4, ..., x_n); – If I′(aux_1) = I′(aux_2) = 0 then I |= AMT(x_1, x_2, x_3) and I |= -x_4 & ... & -x_n; – If I′(aux_1) = 0 and I′(aux_2) = 1 (or vice versa) then I |= AMO(x_1, x_2, x_3) and I |= AMO(x_4, ..., x_n). 3b) Write all clauses for encoding AMT(x_1, x_2, x_3, aux_1, aux_2) with no more auxiliary variables. Answer 3b: ... We need one clause for each subset of 3 elements out of 5, that is, binomial(5,3) = 10 clauses: -x_1 v -x_2 v -x_3, -x_1 v -x_2 v -aux_1, -x_1 v -x_2 v -aux_2, -x_1 v -x_3 v -aux_1, -x_1 v -x_3 v -aux_2, -x_1 v -aux_1 v -aux_2, -x_2 v -x_3 v -aux_1, -x_2 v -x_3 v -aux_2, -x_2 v -aux_1 v -aux_2, -x_3 v -aux_1 v -aux_2. 3c) How many clauses and auxiliary variables are needed in total for this Heule-3 encoding of AMT(x_1, ..., x_n)? Suposse, as said for AMO, that the value of n is much larger than the base case, where polinomic encoding is used. Answer 3c: ... The part AMT(-aux_1, -aux_2, x_4, ..., x_n) has one literal less. So, to eliminate one literal, we need 10 clauses and 2 auxiliary variables, and hence in total, we need approximately 10n clauses and 2n auxiliary variables. -------------------------------------------------------------------------------------------------- _____________________________________________________________________________________ _____________________________________________________________________________________ FIRST-ORDER LOGIC: _____________________________________________________________________________________ _____________________________________________________________________________________ Problem 4. (3 points). Let F be the first-order formula Ex Ay Ez (p(z, y) & -p(x, y) ). 4a) Give a model I of F with D_I = {a, b, c}. Answer 4a: ... Intuitively, we can build the model by considering, for example, that the x that exists is a. Then we need that -p(x,y) for all y, that is, p_I(a, a) = 0 p_I(a, b) = 0 p_I(a, c) = 0 Furthermore, we need that for all y, there exists a z such that p(z,y), which we can achieve by always taking the same z (this is not necessary, but here it works): p_I(b, a) = 1 p_I(b, b) = 1 p_I(b, c) = 1 This gives us a model, independently of how we define the remaining three cases: p_I(c, a) p_I(c, b) p_I(c, c) 4b) Give a model I of F with an infinite domain D_I. Answer 4b: ... D_I = N (the natural numbers) p_I(n,m) = n > m ------------------------------------------------------------------------------------ Problem 5. (3 points). 5a) Write a formula F of FOLE, built only over the equality predicate and one unary predicate symbol p, ("unary" means that the arity of p is 1; use NO other function, constant, or predicate symbols) such that I |= F iff p is true for EXACTLY 2 elements of D_I. Answer 5a: ... F = Ex Ey ( ( -(x=y) & p(x) & p(y) ) & Az ( p(z) -> z=x v z=y ) ) Alternative formulas: F = Ex Ey Az ( p(z) -> z=x v z=y ) & Ex Ey (-(x=y) & p(x) & p(y) ) ---------- at most 2 --------- ---------- at least 2 --------- 5b) Let s and p be two binary function symbols. Consider the two first-order interpretations I1 and I2: D_I1 = R (the real numbers), s_I1(n,m) = n+m, p_I1(n,m) = n*m D_I2 = C (the complex numbers), s_I2(n,m) = n+m, p_I2(n,m) = n*m Below, complete the formula F of FOLE with NO other function or predicate symbol than s, p, and equality, such that F distinguishes I1 and I2, i.e., such that F is true in one of I1 or I2 and false in the other. F : Ey Ez ( (Ax p(x,y) = ...) & p(z,z) = ... ) "Hint: note that for any real or complex numbers u,v, the equalitv uv = 2uv + u holds iff -(uv) = u." Answer 5b: ... *Note*: Of course, it makes no sense to write a (sub)formula like Ax Ey s(x,y) = 0, because 0 is not a symbol of the syntax of F; it is a domain element. We express the existence of the square root z of a negative number, which does not hold in the real numbers, using the part Ez p(z,z) = ... . We express that y is −1 using the part Ey (Ax p(x,y) = ...): make xy = 2xy + x, which implies -(xy) = x. Writing xy = 2xy + x as p(x,y) = s(s(p(x,y), p(x,y)), x), we get: F : Ey Ez ( (Ax p(x,y) = s(s(p(x,y), p(x,y)), x)) & p(z,z) = y) Another answer: We force y = 1 and then z^2 = y + 2*z^2, which implies z^2 = -y. F : Ey Ez ( (Ax p(x,y) = x) & p(z,z) = s(y, s(p(z,z), p(z,z))) ) ------------------------------------------------------------------------------------ Problem 6. (4 points). Formalize and prove by resolution that sentence D is a logical consequence of the other three: A: Everybody loves his father and his mother. B: Mary is clever. C: When someone is clever, at least one of his parents is clever too. D: There are clever people who are loved by someone. Mandatory: 1. use function symbols f(x) and m(x) meaning "father of x" and "mother of x", and the constant function symbol mary. 2. use predicate symbols loves(x,y) meaning "x loves y", and isclever(x) meaning "x is clever". Answer 6.a: A) ... B) ... ... A) Ax (loves(x,f(x)) & loves(x,m(x)) B) isclever(mary) C) Ax (isclever(x) -> (isclever(f(x)) v isclever(m(x)))) -D) -(Ex Ey (isclever(x) & loves(y,x))) Transformed into clausal form, we obtain the clauses: *Note*: use different variable names in each clause x1,y1,.. for the first clause, x2,y2,... for the second, etc. Answer 6.b: ... A1. loves(x1,f(x1)) A2. loves(x2,m(x2)) B. isclever(mary) C. -isclever(x4) v isclever(f(x4)) v isclever(m(x4)) -D. -isclever(x5) v -loves(y5,x5) By resolution, we obtain the empty clause as follows: Answer 6.c: From: ... + ..., mgu(..., ...) = {...} N. ... VARIABLES in new clause N must be RENAMED: xN,yN,... ... From: B + C, mgu(isclever(mary), isclever(x4)) = {x4=mary} 6. isclever(f(mary)) v isclever(m(mary)) From: 6 + -D, mgu(isclever(f(mary)), isclever(x5)) = {x5=f(mary)} 7. isclever(m(mary)) v -loves(x7,f(mary)) with y5 renamed to x7 From: 7 + -D, mgu(isclever(m(mary)), isclever(x5)) = {x5=m(mary)} 8. -loves(x8,f(mary)) v -loves(y8,m(mary)) with x7 renamed to x8, and y5 renamed to y8 From: A1 + 8, mgu(loves(x1,f(x1)), loves(x8,f(mary)))= {x1=mary, x8=mary} 9. -loves(x9,m(mary)) with y8 renamed to x9 From: A2 + 9, mgu(loves(x2,m(x2)), loves(x9,m(mary))) = {x2=mary, x9=mary} 10. []