-------------------------------------------------------------------------------------------------- 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 -------------------------------------------------------------------------------------------------- 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: ... 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: ... -------------------------------------------------------------------------------------------------- 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 I′ |= AMT(x_1, x_2, x_3, aux_1, aux_2) & AMT(-aux_1, -aux_2, x_4, ..., x_n) then, Answer 3a2: ... 3b) Write all clauses for encoding AMT(x_1, x_2, x_3, aux_1, aux_2) with no more auxiliary variables. Answer 3b: ... 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: ... -------------------------------------------------------------------------------------------------- _____________________________________________________________________________________ _____________________________________________________________________________________ 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: ... 4b) Give a model I of F with an infinite domain D_I. Answer 4b: ... ------------------------------------------------------------------------------------ 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: ... 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: ... ------------------------------------------------------------------------------------ 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) ... ... 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: ... 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,... ...