-------------------------------------------------------------------------------------------------- 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 -------------------------------------------------------------------------------------------------- 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: ... 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: ... -------------------------------------------------------------------------------------------------- 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: ... } Prove that this procedure is correct, i.e., C |= D iff , and express the below. Answer 3.b: : ... <= Prove that if then C |= D. Answer 3.c: ... => Hint: prove it by contraposition (contradiction): if not() then not(C |= D). Answer 3.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: ... 4b) Is F a logical consequence of G? Answer 4.b: ... 4c) Are F and G logically equivalents? Answer 4.c: ... ------------------------------------------------------------------------------------ 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: ... 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: ... * Formula B: F2 Answer 5.b.B: ... * Formula C: -F1 & F3 Answer 5.b.C: ... * Formula D: -F1 & F4 Answer 5.b.D: ... * Formula E: -F3 & -F4 & F5 Answer 5.b.E: ... * Formula F: -F5 Answer 5.b.F: ... ------------------------------------------------------------------------------------ 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) ... ... Transformed in clausal form, we get the clauses: Answer 6.b: ... By resolution, we obtain the empty clause as follows: Answer 6.c: N From: mgu: New clause: rename variables 1. ... + ... mgu(..., ...) = {...} 1. ... ...