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

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


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

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

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


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

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

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


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

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

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

      2) not (I′ |= Ck) for some k in 1..n. Then, ... 
>>> Answer 4b2)
    ...