-------------------------------------------------------------------------------------------------- Logic in Computer Science, November 4th, 2025. Time: 2h00min. No books or lecture notes allowed. -------------------------------------------------------------------------------------------------- - Insert your answers on the dotted lines ... below, and only there. - 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., etc like in: I |= p & (q v -r) (the interpretation I satisfies the formula p & (q v -r) ). You can write not (I |= F) to express "I does not satisfy F", or not (F |= G) to express "G is not a logical consequence of F" Also you can use subindices with "_". For example write x_i to denote x-sub-i. -------------------------------------------------------------------------------------------------- Problem 1. (2.5 points). 1a) Is it true that for any two propositional formulas F and G, we have that F and G are logically equivalent iff (F & -G) v (G & -F) is unsatisfiable? Prove it using only the definition of propositional logic. >>> Answer 1a): ... (F & -G) v (G & -F) is unsatisfiable iff [by def. of unsatisfiable] AI, not (I |= (F & -G) v (G & -F)) iff [by def. of |=] AI, eval_I((F & -G) v (G & -F)) = 0 iff [by def. of eval_I(v)] AI, max(eval_I(F & -G), eval_I(G & -F)) = 0 iff [by def. of eval_I(&)] AI, max(min(eval_I(F),eval_I(-G)), min(eval_I(G),eval_I(-F))) = 0 iff [by def. of eval_I(-)] AI, max(min(eval_I(F),1-eval_I(G)), min(eval_I(G),1-eval_I(F))) = 0 iff [by the following case analysis:] eval_I(F) eval_I(G) max(min(eval_I(F),1-eval_I(G)), min(eval_I(G),1-eval_I(F))) 0 0 0 0 1 1 1 0 1 1 1 0 The expression max(min(eval_I(F),1-eval_I(G)), min(eval_I(G),1-eval_I(F))) equals 0 only when eval_I(F) and eval_I(G) are both 0 or both 1, that is, when eval_I(F) = eval_I(G]. So, AI, max(.....) = 0 is true iff AI, eval_I(F) = eval_I(G) iff [by def. of eval_I (only be 0 or 1)] AI, eval_I(F) = 1 iff eval_I(G) = 1 iff [by def. of |=] AI, I |= F iff I |= G iff [by def. of model] AI, I is model of F iff I is model of G iff [by del. of logical equivalence] F === G 1b) Is it true that for any two propositional formulas F and G, we have that G is a logical consequence of F iff the formula F -> G is satisfiable? Prove it using only the definition of propositional logic. >>> Answer 1b): ... This is false. Let F be the formula p v q, and let G be the formula p & q. The formula F -> G = p v q -> p & q is satisfiable: The interpretation I(p) = I(q) = 0 is a model of p v q -> p & q = -(p v q) v (p & q). But we have that not (p v q |= p & q). For example, I'(p) = 1, I'(q) = 0 is a model of F = p v q, but is not a model of G = p & q. -------------------------------------------------------------------------------------------------- Problem 2. (2.5 points). 2a) Given a literal l, we denote by var(l) its variable, that is, var(p) = var(-p) = p for any propositional variable p. We also say that any two clauses of the form p v C and -p v D respectively for a certain propositional variable p can be resolved with respect to p, and their resolution is the clause C v D. Let C1, C2 be two clauses. Prove that if there are two different literals l and l' in C1 such that C1 and C2 can be resolved with respect to var(l) and also with respect to var(l') then their resolution in both cases is a tautology. >>> Answer 2a) ... Since l is in C1, and C1 and C2 can be resolved with respect to var(l), then -l belongs to C2. Similarly, -l' belongs to C2. As l and l' are different literals, l' belongs to C1 \ {l}, and -l' belongs to C2 \ {-l}. Therefore the resolution of C1 and C2 with respect to var(l) contains both l' and -l'. So it is a tautology. The same argument applies to prove that the resolution of C1 and C2 with respect to var(l') is a tautology too. 2b) Consider the following particular case of the resolution ("unitary" resolution): p -p v C -------------- C where p is a propositional symbol. Prove that the "unitary" resolution is not refutationally complete for clauses that are not Horn. >>> Answer 2b) ... Counterexample: C1: p v q C2: p v -q C3: -p v q C4: -p v -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. -------------------------------------------------------------------------------------------------- Problem 3. (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, so in total we need n/2 variables and 3n clauses. We now want to extend the encoding for at-most-two (amt, also written x1 + ... + xn <= 2). Let us prove that amt(x1 ... xn) has a model I iff amt(x1, x2, x3, aux1, aux2) AND amt(-aux1, -aux2, 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. * amt(x1 ... xn) has a model I ==> amt(x1, x2, x3, aux1, aux2) AND amt(-aux1, -aux2, x4, ..., xn) has a model I′: If I |= amt(x1, ..., xn) and k is the number of literals of {x1, x2, x3} that are true in I, then we *extend* I into I′ as follows: >>> Answer 3a) ... - if k = 0 we set I′(aux1) = I′(aux2) = 1; - if k = 1 we set (for example) I′(aux1) = 1 and I′(aux2) = 0; - if k = 2 we set I′(aux1) = I′(aux2) = 0. In all three cases I′ |= amt(x1, x2, x3, aux1, aux2) AND amt(-aux1, -aux2, x4, ..., xn). * amt(x1 ... xn) has a model I <== amt(x1, x2, x3, aux1, aux2) AND amt(-aux1, -aux2, x4, ..., xn) has a model I′: If I′ |= amt(x1, x2, x3, aux1, aux2) AND amt(-aux1, -aux2, x4, ..., xn) then ... >>> Answer 3b) ... "forgetting" the part of the auxiliary variables, in all cases the resulting I is a model of amt(x1, ..., xn), because: – if I′(aux1) = I′(aux2) = 1 then I |= -x1 & -x2 & -x3 and I |= amt(x4, ..., xn) – if I′(aux1) = I′(aux2) = 0 then I |= amt(x1, x2, x3) and I |= -x4 & ... & -xn – if I′(aux1) = 0 and I′(aux2) = 1 (or vice versa) then I |= amo(x1, x2, x3) and I |= amo(x4, ..., xn). -------------------------------------------------------------------------------------------------- Problem 4. (2.5 points). Prove the refutational completeness of the resolution, that is, if S is an unsatisfiable set of clauses, then [] in Res(S). Let us prove the contrapositive by induction on the number N of predicate symbols of S: we prove that if [] is not in Res(S), then S is satisfiable by induction on N. Complete adequately the following inductive proof. BASE CASE: If N = 0 (S contains no symbols) then S ... >>> Answer 4a) ... either contains only the empty clause (which is not the case because we would have [] in Res(S)), or contains no clauses at all (and then it is trivially satisfiable). INDUCTIVE CASE: Let N > 0. Let p be a predicate symbol of S. Let SP (S without p) be the set of clauses of S that do not contain the symbol p. Let {p v C1, ... , p v Cn, -p v D1, ... , -p v Dm} be the set of all non-tautological clauses of S with the symbol p. Let S′ = SP U {Ci v Dj | i in 1..n, j in 1..m}, which is a set in which p does not appear; it has N−1 predicate symbols. Since all clauses of S′ are in Res(S), if [] not in Res(S) then [] not in Res(S′). This implies by H.I. that S′ is satisfiable, that is, it has a model I′. We will now see that this implies that S is satisfiable by constructing a model I for S, extending the model I′, which is undefined for p since p does not appear in S′. There are two cases: 1) I′ |= Ci for all i in 1..n. Then the extension I of I′ with ... >>> Answer 4b1) ... I(p) = 0 is a model of S: it satisfies all the (non-tautological) clauses of S that are not in S′, which are those of the set {p v C1, ... , p v Cn, -p v D1, ... , -p v Dm}. 2) not (I′ |= Ck) for some k in 1..n. Then, ... >>> Answer 4b2) ... since S′ contains {Ck v D1, ... , Ck v Dm} and I′ |= S′, we have that I′ |= Dj, for all j in 1..m. Then, as before, the extension I of I′ with I(p) = 1 is a model of S.