--------------------------------------------------------------------------------------------------
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



--------------------------------------------------------------------------------------------------

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)
    ...




  * amo(x1, x2, x3, aux) AND amo(-aux, x4, ..., xn) has a model I′  ==>  amo(x1 ... xn) has a model I:

>>> Answer 2b)
    ...





--------------------------------------------------------------------------------------------------

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)
    ...



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)
    ...




--------------------------------------------------------------------------------------------------


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)
    ...




_____________________________________________________________________________________
_____________________________________________________________________________________

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)
    ...




------------------------------------------------------------------------------------


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)
    ...





------------------------------------------------------------------------------------

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)
    ...




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)
    ...




------------------------------------------------------------------------------------


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)
    ...