-------------------------------------------------------------------------------------------------- Logic in Computer Science, June 13rd, 2024. 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. (2.5 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 *Answer1aList* below. Give no explanations why. Below always F,G,H are formulas and I is an interpretation. *Note*: Wrong answers subtract 0.1 points. Unanswered questions subtract 0.05 points. 1) Resolution is a refutationally complete deductive rule, but it is not complete. 2) Given a set of 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 }|. 3) Given a formula F, the Tseitin transformation of F is a set of clauses that is logically equivalent to F. 4) If F is a tautology, then -F |= F. 5) Given n propositional symbols, there are 4^n classes of logically equivalent formulas. 6) There are infinitely many different formulas that are not logically equivalent, even if there is only one predicate symbol. 7) The Tseitin transformation of a formula F is always a CNF formula with at most 3 literals per clause. 8) Given a formula F in DNF, the Tseitin transformation of F can be exponentially large wrt. |F|. 9) For any formula G such that F |= G we have -F |= -G. 10) There are infinitely many different formulas, even if there is only one predicate symbol. 11) The closure under resolution Res(S) can grow infinitely, even if S is a finite set of clauses. 12) Given I and F, it is decidable in linear time whether eval_I(F) = 0. 13) There are formulas F and G such that F |= G and -F |= G. 14) For any H such that F |= H and G |= H we have F & G |= H. 15) There are known algorithms for deciding in polynomial time whether a given formula in DNF is a tautology. 16) F is satisfiable if, and only if, all logical consequences of F are satisfiable formulas. Answer1aList( -, -, -, -, -, -, -, -, -, -, -, -, -, -, -, - ) 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 Answer1aList( T, F, F, T, F, F, T, F, F, T, F, T, T, T, F, T ) -------------------------------------------------------------------------------------------------- Problem 2. (4 points). 2a) Let F, G, and H be three formulas. Is it true that F & (G v H) is satisfiable iff at least one of the formulas F & G and F & H are satisfiable? Prove it as simply as you can using only the definitions of propositional logic. Answer 2.a: ... F & (G v H) is satisfiable [ by def. of satisfiable ] F & (G v H) has a model [ by def. of model ] E I, I |= F & (G v H) [ by def. of |= ] E I, eval_I(F & (G v H)) = 1 [ by def. of eval_I( & ) ] E I, min(eval_I(F), eval_I(G v H)) = 1 [ by def. of eval_I( v ) ] E I, min(eval_I(F), max(eval_I(G), eval_I(H))) = 1 [ by def. of min/max ] E I, min(eval_I(F), eval_I(G)) = 1 or min(eval_I(F), eval_I(H)) = 1 [ by def. of eval_I( & ) ] E I, eval_I(F & G) = 1 or eval_I(F & H) = 1 [ by associativity of or ] E I, eval_I(F & G) = 1 or E I, eval_I(F & H) = 1 [ by def. of |= ] E I, I |= F & G or E I I |= F & H [ by def. of model ] F & G has a model or F & H has a model [ by def. of satisfiable ] F & G is satisfiable or F & H is satifiable 2b) Let F be a formula without any *not* (-) connective. Prove that F is satisfiable. Hint: first define an interpretation I, and apply induction on |F|. Answer 2.b: ... Let I be the interpretation where I(p) = 1 for all symbol p in the vocabulary P. We prove that I |= F by induction on |F|, the length of F. Base case: if |F| = 1, F is a predicate symbol p, and I |= p. Induction case: if |F| > 1, F is of the form (F1 & F2) or of the form (F1 v F2), and by induction hypothesis we have I |= F1 and I |= F2, that is, eval_I(F1) = eval_I(F2) = 1. But then max(eval_I(F1),eval_I(F2)) = min(eval_I(F1),eval_I(F2)) = 1 , hence in both cases I |= F. -------------------------------------------------------------------------------------------------- Problem 3. (3.5 points). In a SAT solver we want to implement a procedure bool implies(clause C, clause D) that, given two clauses C and D, returns whether C |= D holds or not, i.e., whether D is a logical consequence of C or not. In our library we have the following procedures: bool is_empty(clause C) // returns whether clause C is empty or not bool is_tautology(clause C) // returns whether clause C is a tautology or not bool contained(clause C, clause D) // returns whether clause C (as a set of literals) // is a subset of clause D (as a set of literals) Implement the procedure 'implies' using the procedures 'is_empty', 'is_tautology' and 'contained' and prove that it is correct. Answer only in the dotted lines that follow the "Answer 3.x" marks below. bool implies(clause C, clause D) { // D is a logical consequence of C Answer 3.a: ... return is_empty(C) or is_tautology(D) or contained(C, D); } Prove that this procedure is correct, i.e., C |= D iff , and express the below. Answer 3.b: : ... : C is empty or D is a tautology or C is a subset of D <= Prove that if then C |= D. Answer 3.c: ... If C is empty, or D is a tautology, or C is a subset of D, then C |= D. If C is empty, then it is false, and it has no models. So trivially, any model of C is a model of D; that is, C |= D. If D is a tautology, then it is satisfied by any interpretation. So trivially, any model of C is a model of D, that is, C |= D. If C is a subset of D, then D is of the form C v C', where C' are the rest of the literals in D but not in C. Now if I is a model of C, that is, I |= C, we have that I |= C v C', i.e., I |= D. Since I was arbitrary, we have that C |= D. => Hint: prove it by contraposition (contradiction): if not() then not(C |= D). Answer 3.d: ... If C is not empty, D is not a tautology, and C is not a subset of D, then not(C |= D). Let D = {l_1, l_2, ..., l_n}. Since D is not a tautology, the assignment I such that I(l_i) = 0 for 1 <= i <= n is well-defined. Now, as C is not empty, and C is not a subset of D, there is a literal l in C but not in D. If l is already defined by I, then it must be I(l) = 1. And if l is not defined by I, we "extend" it so that I(l) = 1. Altogether I is a model of C, and I is not a model of D. Hence not(C |= D). -------------------------------------------------------------------------------------------------- _____________________________________________________________________________________ _____________________________________________________________________________________ FIRST-ORDER LOGIC: _____________________________________________________________________________________ _____________________________________________________________________________________ Problem 4. (3 points). 4) Let F be the formula Ax Ey p(x,f(y)), and let G be the formula Ey Ax p(f(x), y). 4a) Is G a logical consequence of F? Answer 4.a: ... Let's see that not(F |= G). The following interpretation I satisfies that I |= F and not(I |= G): D_I = {a,b} f_I(x) = x // the identity function p_I(a,a) = 0 p_I(a,b) = 1 p_I(b,a) = 1 p_I(b,b) = 0 4b) Is F a logical consequence of G? Answer 4.b: ... Let's see that not(G |= F). The following interpretation I satisfies that I |= G and not(I |= F): D_I = {a,b} f_I(x) = a // the constant function a p_I(a,a) = 0 p_I(a,b) = 1 p_I(b,a) = 0 p_I(b,b) = 0 4c) Are F and G logically equivalents? Answer 4.c: ... From 4a or 4b we have that not(F === G). ------------------------------------------------------------------------------------ Problem 5. (4 points). 5a) Consider the following function symbols and meanings: p of arity 1: p(n) means n-1 and the following predicate symbols: eq of arity 2: eq(n,m) means n is equal to m le of arity 2: le(n,m) means n is less than or equal to m Express in FOL with these symbols the following sentence (which happens to be true in integer arithmetic): "Given any two numbers x and y, if x < y then x <= y-1" Answer 5.a: ... Ax Ay (-eq(x,y) & le(x,y) -> le(x,p(y))) 5b) Consider the following function symbols in a First Order Logic with Equality (FOLE): f of arity 1 g of arity 1 Given the formulas: F1: Ax (f(x) = g(x)) F2: Ax Ay (f(x) = g(y)) F3: Ax Ey (f(x) = g(y)) F4: Ex Ay (f(x) = g(y)) F5: Ex Ey (f(x) = g(y)) Give models for each of the following formulas. Give no explanation. All models must have the domain D_I = Z (the set of integers). * Formula A: F1 & -F2 Answer 5.b.A: ... f_I(n) = n, g_I(n) = n * Formula B: F2 Answer 5.b.B: ... f_I(n) = 0, g_I(n) = 0 * Formula C: -F1 & F3 Answer 5.b.C: ... f_I(n) = 0, g_I(n) = n * Formula D: -F1 & F4 Answer 5.b.D: ... f_I(n) = n, g_I(n) = 0 * Formula E: -F3 & -F4 & F5 Answer 5.b.E: ... f_I(n) = n, g_I(n) = n^2 * Formula F: -F5 Answer 5.b.F: ... f_I(n) = 0, g_I(n) = 1 ------------------------------------------------------------------------------------ Problem 6. (3 points). Formalize and prove by resolution that sentence E is a logical consequence of the other four. A: All teachers sometimes lie. B: Students' friends never lie. C: John is a student. D: John has friends that are teachers. E: LI has been one of the most enjoyable subjects in this course. Formalize the sentences using these predicates: tea(x): "x is a teacher" lie(x): "x sometimes lies" stu(x): "x is a student" fri(x,y): "x is friend of y" john: "the constant John" Answer 6.a: A) ... B) ... ... Obviously E has nothing to do with A-D. So the only way to prove that E is a logical consequence is to prove that A & B & C & D is unsatisfiable. Formalising: A) Ax (tea(x) -> lie(x)) B) Ax (Ey (stu(y) & fri(y,x)) -> -lie(x)) C) stu(john) D) Ex (tea(x) & fri(john,x)) Transformed in clausal form, we get the clauses: Answer 6.b: ... A) -tea(x1) v lie(x1) B) -stu(y2) v -fri(y2,x2) v -lie(x2) C) stu(john) D1) tea(c4) D2) fri(john,c4) By resolution, we obtain the empty clause as follows: Answer 6.c: N From: mgu: New clause: rename variables 1. ... + ... mgu(..., ...) = {...} 1. ... ... 1. D1 + A mgu(tea(c4), tea(x1)) = {x1=c4} 1. lie(c4) 2. 1 + B mgu(lie(c4), lie(x2)) = {x2=c4} 2. -stu(y7) v -fri(y7,c4) 3. C + 2 mgu(stu(john), stu(y7)) = {y7=john} 3. -fri(john,c4) 4. D2 + 3 mgu(fri(john,c4), fri(john,c4)) = {} 4. [] Or using the deductive rule format: D1. tea(c4) A. -tea(x1) v lie(x1) ---------------------------------------------------- with mgu(tea(c4), tea(x1)) = {x1=c4} 1. lie(c4) 1. lie(c4) B. -stu(y2) v -fri(y2,x2) v -lie(x2) ---------------------------------------------------- with mgu(lie(c4), lie(x2)) = {x2=c4} 2. -stu(y7) v -fri(y7,c4) C. stu(john) 2. -stu(y7) v -fri(y7,c4) ---------------------------------------------------- with mgu(stu(john), stu(y7)) = {y7=john} 3. -fri(john,c4) D2. fri(john,c4) 3. -fri(john,c4) ---------------------------------------------------- with mgu(fri(john,c4), fri(john,c4)) = {} 4. []