-------------------------------------------------------------------------------------------------- Logic in Computer Science, Juny 10th, 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) F is satisfiable if, and only if, all logical consequences of F are satisfiable formulas. 2) If F v G |= H then F & -H is unsatisfiable. 3) If there are n propositional symbols, there are 2^(2^n) different clauses 4) If H is not a logical consequence of F & G then F & G & H is unsatisfiable. 5) The closure under resolution of a set of clauses S, Res(S), always has a number of clauses that is quadratic in the size of S. 6) If F is a tautology, then -F |= F. 7) There are infinitely many different formulas that are not logically equivalent, even if there is only one predicate symbol. 8) If F |= G then every model of G is a model of F. 9) It is decidable in polynomial time whether a given formula in DNF is satisfiable. 10) For every F, it does exist G such that not(F |= G). 11) There are formulas F and G such that F |= G and F |= -G. 12) For any formula G such that F |= G we have -F |= -G. 13) Given a formula F, the Tseitin transformation of F always has a number of clauses that is linear in the size of F. 14) Given I and F, it is decidable in linear time whether I |= F. 15) If F is a tautology, then for every G we have F |= G. 16) It is decidable in polynomial time whether a given formula is a tautology. 0 1 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 Answer1List( -, -, -, -, -, -, -, -, -, -, -, -, -, -, -, - ) >>> Answer 1: Answer1List( T, T, F, F, F, T, F, F, T, T, T, F, T, T, F, F) -------------------------------------------------------------------------------------------------- Problem 2. (2 points). Let F and G be two formulas such that F |= G. Is it true that F is logically equivalent to F & G? (F === F & G) >>> Answer 2a) F |= F & G ? ... Let J be any model of F. Since F |= G, J is also a model of G. Hence eval_J(F) = eval_J(G) = 1. It follows that eval_J(F & G) = min(eval_J(F), eval_J(G)) = min(1,1) = 1. Therefore, J |= F & G. >>> Answer 2b) F & G |= F ? ... Let J be a model of F & G. Then eval_J(F & G) = min(eval_J(F), eval_J(G)) = 1. Hence, eval_J(F) = 1, and therefore J |= F. -------------------------------------------------------------------------------------------------- Problem 3. (3 points). Let F and G be arbitrary formulas. Is it true that F |= G iff F -> G is a tautology? Prove your answer by providing a proof or a counterexample using only the definitions of propositional logic. >>> Answer 3) ... F -> G is a tautology iff [by def. of ->] -F v G is a tautology iff [by def. of tautology] AI, I |= -F v G iff [by def. of |=] AI, eval_I(-F v G) = 1 iff [by def. of eval_I( v )] AI, max(eval_I(-F), eval_I(G)) = 1 iff [by def. of eval_I( - )] AI, max(1-eval_I(F), eval_I(G)) = 1 iff [by def. of max] AI, 1-eval_I(F) = 1 or eval_I(G) = 1 iff [by arithmetic] AI, eval_I(F) = 0 or eval_I(G) = 1 iff [by def. of |=] AI, not(I |= F) or I |= G iff [by def. of implies] AI, I |= F implies I |= G iff [by def. of logical consequence] AI, F |= G -------------------------------------------------------------------------------------------------- Problem 4. (2.5 points). Given a set of clauses S, the following procedure returns a new set of clauses S3 (not necessarily over the same set of predicate symbols), where the clauses of S3 have at most 3 literals, i.e., S3 is a 3-CNF formula. Moreover, S and S3 are two *equisatisfiable* sets of clauses. Let S = C U Sr, where C = l v l' v C1 is a clause of S with 4 o more literals, and Sr is the rest of clauses. The clauses of a new set S' are obtained from S by incorporating a new predicate symbol p which has the following meaning: p is equivalent to l v l' (p <-> l v l'). In S', the clause C = l v l' v C1 is "substituted" by C' = p v C1 (which has one less literal). Additionally, the relationship p <-> l v l' will be expressed by three additional clauses: 1) -p v l v l' (p -> l v l') 2) p v -l (l -> p) 3) p v -l' (l'-> p) A 3-CNF final set S3 will be obtained by repeating this substitution (with other new symbols p) in clauses of S' with more than three literals. It remains to prove that S and S3 are equisatisfiable. Since S3 is obtained from S through a sequence of transformation steps, it is sufficient to prove that each transformation step preserves equisatisfiability: 4a) S is satisfiable (has a model J) implies S' is satisfiable (it can be found a model J' for S') >>> Answer 4a) ... We can properly extend the interpretation J: * if J |= l v l' then let J' the interpretation that extends J with J'(p) = 1, (J' is like J, except that in addition J'(p) = 1). * if not(J |= l v l'), then let J' the interpretation that extends J with J'(p) = 0. We have that J' |= Sr, because J |= Sr. Additionally, J' |= { p v C1, -l v p, -l' v p, -p v l v l' } because (among other reasons) J |= l v l' v C1. Therefore, J' |= S', and hence S' is satisfiable. 4b) S' is satisfiable (has a model J') implies S is satisfiable (it can be found a model J for S) >>> Answer 4b) ... Let J' be a model of S'. Let J be the restriction on J' "forgetting" the interpretation of p. Thus, whether J'(p) = 0 or J'(p) = 1, we have J |= l v l' v C1. Therefore, J |= S, and hence S is satisfiable. _____________________________________________________________________________________ _____________________________________________________________________________________ FIRST-ORDER LOGIC: _____________________________________________________________________________________ _____________________________________________________________________________________ Problem 5. (2.5 points). @n@nota5: Give two different models of the formula Ax Ey ( p(f(x,y),y) & -p(x,y) ) 5a) The first one should have the smallest possible cardinality. >>> Answer 5a) ... There is no model with cardinality 1. D_I={a,b} p_I(x,y) = (x=y) p_I(a,a)=1 p_I(a,b)=0 p_I(b,a)=0 p_I(b,b)=1 f_I(x,y) = y f_I(a,a)=a f_I(a,b)=b f_I(b,a)=a f_I(b,b)=b if x=a then pick y=b if x=b then pick y=a There is no model with one single element: D_I = {a} P_I(a,a) = 0/1 f_I(a,a) = a that satisfies the formula Ax Ey ( p(f(x,y),y) & -p(x,y) ) because p(a,a) & -p(a,a) is always false. 5b) The second one should have infinite cardinality. >>> Answer 5b) ... D_I=Z (the integer numbers) p_I(n,m) == |n-m|<10 // the distance between n and m is less than 10 f_I(n,m) == m // returns its second argument Pick always y=x+10: Ax ( p(f(x,y),y) & -p(x,y) ) Ax ( |(x+10)-(x+10)| < 10 & |x-(x+10)| >= 10 ) Another solutions for 5b) * D_I = (0, +oo) in the real numbers p_I(x,y) == x >= y f_I(x,y) == 2x For all x > 0 there is an y > 0 (e.g., 2x) such that Ax ( 2x >= 2x and x < 2x ) * D_I = N (the natural numbers) p_I(x,y) == ((x mod 2) = (y mod 2)) // same parity f_I(x,y) == x+1 For all x there is an y (e.g., x+1) such that Ax (((x+1) mod 2 = (x+1) mod 2) & (x mod 2 != (x+1) mod 2) ) ------------------------------------------------------------------------------------ Problem 6. (2.5 points). Prove that Skolemization in general does not preserve logical equivalence. Consider the formula Ax Ey p(x,y) and its Skolemized form. Define an interpretation I with D_I = {a,b} and show that one formula is satisfied while the other is not. >>> Answer 6) ... The Skolemized formula is Ax p(x,f(x)). Let us define the interpretation I as follows: D_I = {a,b} // p_I is the equality relation p_I(a,a) = 1 p_I(a,b) = 0 p_I(b,a) = 0 p_I(b,b) = 1 // f_I returns the other element of D_I f_I(a) = b f_I(b) = a It is easy to see that I |= Ax Ey p(x,y) (always picking y=x), but not(I |= Ax p(x,f(x))), because, for example, p(a,b) is false. Therefore, the formulas are not logically equivalent. ------------------------------------------------------------------------------------ Problem 7. (2 points). Write a formula F of FOL with equality (FOLE), built only over the equality predicate such that any model I of F has a domain D_I with either 2 or 3 elements, that is, I |= F implies 2 <= |D_I| <= 3 >>> Answer 7) ... Ex Ey -(x=y) // At least 2 elements & Ex Ey Ez Au ( u=x v u=y v u=z ) // At most 3 elements ------------------------------------------------------------------------------------ Problem 8. (3 points). Formalize the following sentences in first-order logic and prove by resolution that the last sentence (G) is a logical consequence of the others A & B & C & D & E & F. A: All people who have electric cars are ecologists. B: If someone has a grandmother, then that someone has a mother whose mother is that grandmother. C: A person is an ecologist if their mother is an ecologist. D: Mary is John's grandmother. E: Mary has an electric car. F: John is not an ecologist. G: Mexico will win the FIFA World Cup. Only these predicate symbols may be used: hasEcar(x) means "x has an electric car" isEcologist(x) means "x is an ecologist" mother(x,y) means "y is the mother of x" grandma(x,y) means "y is the grandmother of x" >>> Answer 8) ... Obviously G has nothing to do with A-F. So the only way to prove that G is a logical consequence is to demonstrate that A & B & C & D & E & F is unsatisfiable. Formalization: A: Ax (hasEcar(x) -> isEcologist(x)) B: AxAz (grandma(x,z) -> Ey (mother(x,y) & mother(y,z))) C: AxAy ((mother(x,y) & isEcologist(y)) -> isEcologist(x)) D: grandma(john,mary) E: hasEcar(mary) F: -isEcologist(john). The following clauses are obtained (Clausal Normal Form): A: -hasEcar(x) v isEcologist(x) B yields: AxAz (-grandma(x,z) v Ey (mother(x,y) & mother(y,z))) after Skolemization (where f(x,z) represents the mother): AxAz (-grandma(x,z) v (mother(x, f(x,z)) & mother(f(x,z), z))) which splits, by distributivity, into two clauses: B1: -grandma(x,z) v mother(x, f(x,z)) B2: -grandma(x,z) v mother(f(x,z), z) C: -mother(x,y) v -isEcologist(y) v isEcologist(x) D: grandma(john,mary) E: hasEcar(mary) F: -isEcologist(john) Doing resolution steps (number the new clauses from 1): Num From mgu New clause 1 E + A {x = mary} isEcologist(mary) 2 D + B1 {x = john, z = mary} mother(john, f(john,mary)) 3 D + B2 {x = john, z = mary} mother(f(john,mary), mary) 4 2 + C {x = john, y = f(john,mary)} -isEcologist(f(john,mary)) v isEcologist(john) 5 4 + F {} -isEcologist(f(john,mary)) 6 3 + C {x = f(john,mary), y = mary} -isEcologist(mary) v isEcologist(f(john,mary)) 7 6 + 5 {} -isEcologist(mary) 8 1 + 7 {} [] (Empty clause)