June 17th, 2026

Problem 1. (21 points)

Instruction

Let $F$ be the propositional formula:

$$\left((p\wedge q)\to (r\vee q)\right)\to \neg \left(\neg (p\leftrightarrow q)\to (r\vee q)\right)$$

1. Which atoms are pure in $F$? Justify your answer.
2. Compute a clausal normal form $C$ of $F$ by applying the CNF transformation algorithm with naming and optimisation-based on polarities of subformulas.
3. Decide the satisfiability of the computed CNF formmula $C$ by applying the DPLL method to $C$. If $C$ is satisfiable, give an interpretation which satisfies it.

Problem 2. (10 points)

Instruction

Consider a finite set $S$ of clauses such that no clause contains a positive literal. Is satisfiability of $S$ decidable without splitting? If yes, give an algorithm and argue for its correctness. If no, give a counterargument.

Problem 3. (12 points)

Does the following entailment hold?

• If a robot $A$ completed a task, then, if robot $B$ reached the charging station, then robot $C$ delivered the package.
• Robot $B$ reached the charging station.
• Thus, either robot $A$ does not complete the task or robot $C$ delivered the package (or robot $A$ does not complete the task and robot $C$ delivered the package).

Give a proof or provide a countermodel.

Problem 4. (15 points)

Instruction

Consider the first-order theory

$$\Gamma =\{\forall x(P(x)\to \exists yR(x,y)),\forall x\forall y(R(x,y)\to (\neg Q(x)\vee \neg Q(y)))\}$$

and the following formula $\phi$:

$$\forall a(P(a)\to \neg Q(a)).$$

Does the theory $\Gamma$ entail the formula $\phi$? Answer yes or no.
If yes, provide a first-order tableau proof.
If no, give and explain a countermodel that supports your answer.

Problem 5. (15 points)

Instruction

Let $\Sigma =\{f,a\}$ be a signature, where $f$ is a unary function symbol and $a$ is a constant. Let $\mathcal{T}$ be the theory axiommised by the axioms:

$$\begin{array}{rl}x& =f(y)\\ y& =a\vee x=z\end{array}$$

where $x,y,z$ are variables and thus the above axioms are implicitly universally quantified. The symbol $=$ denotes the standrad equality predicate, axiomatised accordingly by the axioms of the theory of equality ${\mathcal{T}}_E$.

Is $\mathcal{T}$ stably infinite? If so, prove it. If not, disprove it.

Problem 6. (27 points)

Instruction

Let $F$ be the formula

$$L_1\wedge L_2\wedge L_3\wedge (\neg L_4\vee \neg L_5)$$

where

$$\begin{array}{rl}{L}_1& \text{denotes}f(a+3)=f(b)\\ L_2& \text{denotes}a=b-4\\ L_3& \text{denotes}\mathrm{read}\left(\mathrm{write}\right(\mathrm{write}(A,f(b),a),f(a),b),f(b-1))=a\\ L_4& \text{denotes}f(a)=f(b)\\ L_5& \text{denotes}\mathrm{read}(A,f(b-1))=1\end{array}$$

with $a,b$ being integer constants, $f$ being a unary function, $A$ being an integer array, and $+,-,1,3,4$ being interpreted in the standard way over the integers. Further, $\mathrm{read}$ and $\mathrm{write}$ are interpreted over the theory of arrays.

When considering the propositional structure of $F$, assume that DPLL returns the following truth value assignments over the literals of $F$:

• $I_1:$ $L_1,L_2,L_3,L_4\mapsto \top$ and $L_5\mapsto \perp$.
• $I_2:$ $L_1,L_2,L_3,L_5\mapsto \top$ and $L_4\mapsto \perp$.

For each $i\in \{1,2\}$, is $F$ satisfiable when considering the truth value assignment of $I_i$ to the literals of $F$? If it is, provide a theory model of $F$. If not, describe the next step for checking the satisfiability of $F$ using DPLL(T).

When reasoning about theory literals to determine satisfiability of $F$, use the Nelson-Oppen decision procedure to reason in the combination of theories. Use the decision procedures for the theory of uninterpreted functions and the one for arrays, and use simple mathematical reasoning for deriving new equalities among the constants in the theory of linear integer arithmetic. Provide sufficient details on your steps; importantly, state which theory decision procedure you use and detail the steps of each decision procedure. In particular, write down the congruence closures/classes and how you came up with them.