-------------------------------------------------------------------------------------------------- Logic in Computer Science, January 15th, 2026. Time: 3h00min. No books or lecture notes allowed. -------------------------------------------------------------------------------------------------- Note on evaluation: eval(propositional logic) = max(eval(Problems 1,2,3,4), eval(midterm exam)). eval(first-order logic) = eval(Problems 5,6,7,8). - 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. (2.5 points). 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) If F is unsatisfiable then, for every formula G, we have that F |= G. 2) For any formula G such that F |= G we have -F |= -G. 3) F is a tautology iff there exists an interpretation I such that I |= -F. 4) For every clause C different from the empty clause, there exists an interpretation I such that not(I |= C). 5) If F & G |= -H then F & G & H is unsatisfiable. 6) Given F, it is known it is decidable in polynomial time whether F is satisfiable. 7) Given I and F, it is known how to decide in linear time whether I is a minimal model of F, that is, a model I with the minimal number of symbols p such that I(p) = 1. 8) F |= G iff -F v G is a tautology. 9) If S is a set of 2-SAT clauses (that is, clauses with at most two literals), then |Res(S)| is quadratic in |S|. 10) If F is a tautology, then for every G we have G |= F. 11) It is decidable in polynomial time whether a given formula in CNF is a tautology. 12) Resolution is a complete deductive rule, but it is not refutationally complete. 13) The formula p is a logical consequence of (p v r) & (-q v r) & (q v r). 14) There are formulas F and G such that F |= G and F |= -G. 15) The Tseitin transformation of a formula F is always a CNF formula with exactly 3 literals per clause. 16) For every formula F there is a set of clauses S that is logically equivalent to F and such that no clause in S has more than 3 literals. 17) The formula (p v q) & (-p v q) & (-p v -q) & (-q v p) is unsatisfiable. 18) If there are n propositional symbols, there are 4^n (4 to the power n) different clauses Answer1List( -, -, -, -, -, -, -, -, -, -, -, -, -, -, -, -, -, - ) 0 1 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 Answer1List( T, F, F, F, T, F, F, T, T, T, T, F, F, T, F, *, T, T ) (*) This question will not be considered in the grading of this problem. Tseitin's transformation converts any formula F into an equisatisfiable 3-CNF formula; such formulas are not necessarily logically equivalent. However, another procedure could exist. -------------------------------------------------------------------------------------------------- Problem 2. (2.5 points). Let us remember the Heule-3 encoding for at-most-one (amo) that is, for expressing in CNF that at most one of the literals x1 ... xn is true, also written x1 + ... + xn <= 1. It uses the fact that amo(x1, ..., xn) iff amo(x1, x2, x3, aux) AND amo(-aux, x4, ..., xn). Then the part amo(-aux, x4, ..., xn), which has n-2 variables, can be encoded recursively in the same way, and amo(x1, x2, x3, aux) can be expressed using the quadratic encoding with 6 clauses. In this way, for eliminating two variables, we need one auxiliary variable and six clauses. Prove the previously established fact (both formulas are equisatisfiable): amo(x1 ... xn) has a model I iff amo(x1, x2, x3, aux) AND amo(-aux, x4, ..., xn) has a model I′, with I(xi) = I′(xi) for all i in 1..n. Complete adequately the sufficient and necessary implications of the proof below. * amo(x1 ... xn) has a model I ==> amo(x1, x2, x3, aux) AND amo(-aux, x4, ..., xn) has a model I′: Hint: extend properly the interpretation I. >>> Answer 2a) ... Let k be the number of literals in {x1, x2, x3} that are true in I: - if k = 0 we set I′(aux) = 1; - if k = 1 we set I′(aux) = 0. In both cases I′ |= amo(x1, x2, x3, aux) AND amo(-aux, x4, ..., xn). * amo(x1, x2, x3, aux) AND amo(-aux, x4, ..., xn) has a model I′ ==> amo(x1 ... xn) has a model I: >>> Answer 2b) ... "forgetting" the part of the auxiliary variable in I', in all cases the resulting I is a model of amo(x1, ..., xn), because: – if I′(aux) = 1 then I |= -x1 & -x2 & -x3 and I |= amo(x4, ..., xn) – if I′(aux) = 0 then I |= amo(x1, x2, x3) and I |= -x4 & ... & -xn -------------------------------------------------------------------------------------------------- Problem 3. (2.5 points). Let S be a set of clauses and let I be an arbitrary interpretation. Prove that I |= S iff I |= Res(S). 3a) I |= Res(S) ==> I |= S >>> Answer 3a) ... Trivially true, because S is a subset of Res(S) (for def. of Res(S) that is the union of all S_i's). 3b) I |= S ==> I |= Res(S) We have obtained Res(S) from S, adding a finite number of times k, a conclusion by resolution from clauses that you already have. Hint: prove that for all I, I |= S ==> I |= Res(S) by induction on k >>> Answer 3b) ... * If k = 0, it is trivial because then S = Res(S). * If k > 0, assume that the first step is from S to S', adding 1 clause by resolution from S. By correctness of resolution, S |= S' (for any interpretation I we have I |= S ==> I |= S'). Moreover, as S is a subset of S', we have that S' |= S. So, we conclude that S === S'. By induction hypothesis, as the number of steps from S' to Res(S) is k-1, we finally have that I |= S ==> I |= Res(S). Note: it can also be proven by considering the transitivity of ==> * I |= S ==> I |= S' (proven before) * I |= S' ==> I |= Res(S) (by induction hypothesis) -------------------------------------------------------------------------------------------------- Problem 4. (2.5 points). Let F, G, and H denote arbitrary propositional formulas. Is it true that F & (G v H) is satisfiable iff at least one of the formulas F & G or F & H is satisfiable? Prove your answer by providing a proof or a counterexample using only the definitions of propositional logic. >>> Answer 4) ... It is true. F & (G v H) is satisfiable iff [ by def. of satisfiable ] F & (G v H) has a model iff [ by def. of model ] EI, I |= F & (G v H) iff [ by def. of |= ] EI, eval_I(F & (G v H)) = 1 iff [ by def. of eval_I( & ) ] EI, min(eval_I(F), eval_I(G v H)) = 1 iff [ by def. of eval_I( v ) ] EI, min(eval_I(F), max(eval_I(G), eval_I(H))) = 1 iff [ by def. of min, max ] EI, eval_I(F) = 1 and eval_I(G) = 1 or eval_I(F) = 1 and eval_I(H) = 1 iff [ by def. of min ] EI, min(eval_I(F), eval_I(G)) = 1 or min(eval_I(F), eval_I(H)) = 1 iff [ by def. of eval_I( & ) ] EI, eval_I(F & G) = 1 or eval_I(F & H) = 1 iff [ by def. of eval_I ] EI, I |= F & G or I |= F & H iff [ by def. of |= ] F & G has a model or F & H has a model iff [ by def. of satisfiable ] F & G is satisfiable or F & H is satisfiable _____________________________________________________________________________________ _____________________________________________________________________________________ FIRST-ORDER LOGIC: _____________________________________________________________________________________ _____________________________________________________________________________________ Problem 5. (2.5 points). Prove that the Skolemization of an arbitrary formula F, Skol(F), does not preserve the logical equivalence. In order to prove it, it is *mandatory* to use the following formula F = Ax Ey Az (p(x,y) v -q(z,y)) and its transformation Skol(F). Give an interpretation I with the smallest possible cardinality such that I is a model of F and not of Skol(F), or vice versa. Show that no other interpretation J with lower cardinality works for this purpose. Note: the cardinality of an interpretation is the number of elements in its domain. >>> Answer 5) ... The skolemized formula Skol(F) is Ax Az (p(x,f(x)) v -q(z,f(x))) where f is a new skolem function symbol. The smallest possible cardinality of the interpretation I is 2. For example: D_I = {a, b} f_I(a) = b f_I(b) = a p_I(a,a) = 1 p_I(a,b) = 0 p_I(b,a) = 0 p_I(b,b) = 1 q_I(a,a) = 1 q_I(a,b) = 1 q_I(b,a) = 1 q_I(b,b) = 1 Clearly I |= Ax Ey Az (p(x,y) v -q(z,y)) Because for each x exists y s.t. p(x,y) is true. But not(I |= Ax Az (p(x,f(x)) v -q(z,f(x))) For example, for x=a and z=a, Skol(F) is false, i.e. p(a,f(a)) v -q(a,f(a)) is false. So, we can conclude that the formulas F and Skol(F) are not logically equivalent. All four of the interpretations J with only one element in the domain are either models of both formulas or neither. For instance, the following interpretation J: D_J = {a} f_J(a) = a p_J(a,a) = 1 q_J(a,a) = 1 satisfies both formulas F and Skol(F). ------------------------------------------------------------------------------------ Problem 6. (2.5 points). Let F and G be the following formulas in FOL: F = Ax p(a, x) & Ey -q(y) G = Eu Ew (-q(w) & p(u,a)). Do we have F |= G? Prove it by explaining in detail the steps followed in the proof. >>> Answer 6) ... It is true. We will prove that F |= G by proving that F & -G is unsatisfiable, turning it into clausal form S, and obtaining the empty clause from S by resolution and factoring. Here F gives two clauses: 1: p(a,x) 2: -q(c) (here c is the Skolem constant introduced for y) -G is -(Eu Ew (-q(w) & p(u,a))) which becomes Au Aw -(-q(w) & p(u,a)) which becomes Au Aw (q(w) v -p(u,a)) which becomes the clause: 3: q(w) v -p(u,a) By one step of resolution between 1 and 3 with mgu {x = a, u = a} we get clause 4: q(w) and with one more step of resolution between 2 and 4 with mgu {w = c} we get the empty clause. ------------------------------------------------------------------------------------ Problem 7. (3 points). 7a) Consider a binary function symbol s and the following first-order interpretations I and I′: I: where D_I is the set of natural numbers and where s_I(n, m) = n + m. I′: where D_I′ is the set of integer numbers and where s_I′(n, m) = n + m. Write the simplest possible formula F in first-order logic with equality using only the function symbol s and the equality predicate = (no other symbols), such that F is true in one of the interpretations and false in the other one. Provide a brief explanation. >>> Answer 7a) ... F is Ax Ay Ez s(x,z) = y (that is, z, the difference y-x, is defined for all x, y). We have that not(I |= F) and I' |= F. Note: Of course it makes no sense to write anything like Ax Ey s(x,y) = 0, because 0 is not a symbol of the syntax of F; it is a domain element. 7b) Let F be the FOLE formula: Ez p(z) & Ax (p(x) -> Ey (-p(y) & x=f(y,y))) Let I be the interpretation with domain D_I = R (the real numbers), and p_I(x) = 1 iff x > 0 f_I(x,y) = x·y (the product in R) We have I |= F, but if J |= F, how many elements has at least J? Prove it. >>> Answer 7b) ... Since Ez p(z) must hold, there must be an element a in the domain such that p_J(a) = 1. And as Ax (p(x) -> Ey (-p(y) & x=f(y,y))), there must exist an element b such that -p_J(b) and a = f_J(b,b). Since p_J(a) and -p_J(b) must both hold, a and b have to be different. So if J |= F, at least J must have 2 elements. As an example of a model for which this bound is tight, consider the same interpretation as given in the statement, but using D_J = {-1, 1}: p_J(x) = 1 iff x > 0 f_J(x,y) = x·y (the product in R) ------------------------------------------------------------------------------------ Problem 8. (2 points). We want to write a computer program that takes as input two arbitrary first-order formulas F and G and always terminates writing "yes" if F === G, and "no" otherwise. Explain very shortly the steps you would follow to do this, or to get something as similar as possible. >>> Answer 8) ... No such program can exist, since this question is undecidable. It is only semi-decidable: the best one can get is a program that terminates with "yes" if F === G, and otherwise terminates with "no" or does not terminate. Steps for this: 1. Convert (F & -G) v (-F & G) into its clausal form S_0. We have F === G iff S_0 unsat. 2. Compute the closure under resolution+factoring of S_0 by levels, in successive steps for i = 0,1,2,...: 2a: If the empty clause is in S_i, terminate with "yes: F === G". 2b: Otherwise, obtain S_{i+1} by adding to S_i all new clauses one can get by one step of resolution or factoring on clauses in S_i. 2c: If no new clause was obtained from S_i, terminate with "no"; else, go to 2a with the next i.