June 26th, 2024 (1st Exam for SS 2024)

This exam sheet consists of five problems, yielding a total of 100 points. Good luck!

Problem 1. (25 points)

Problem 1. (25 points)

Consider the formula:

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

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

(1) Which atoms are pure in the above formula?

• $(\neg q\wedge r)\wedge \neg ((p\leftrightarrow r)\vee (p\to r))$ (positive)
  • $\neg q\wedge r$ (positive)
    • $\neg q$ (positive)
      • $q$ (negative)
    • $r$ (positive)
  • $\neg ((p\leftrightarrow r)\vee (p\to r))$ (positive)
    • $(p\leftrightarrow r)\vee (p\to r)$ (negative)
      • $p\leftrightarrow r$ (negative)
        • $p$ (mixed)
        • $r$ (mixed)
      • $p\to r$ (negative)
        • $p$ (positive)
        • $r$ (negative)
• $q$: negatively pure
• $p$: impure
• $r$ impure

(2) Compute a clausal normal form $C$ of the above formula by applying the CNF transformation algorithm with naming and optimisation based on polarities of subformulas.

Label	Subformula	Polarity	Generated
$n_1$	$\neg q$	positive	$n_1\to \neg q$
$n_2$	$n_1\wedge r$	positive	$n_2\to (n_1\wedge r)$
$n_3$	$p\leftrightarrow r$	negative	$(p\leftrightarrow r)\to n_3$
$n_4$	$p\to r$	negative	$(p\to r)\to n_4$
$n_5$	$n_3\vee n_4$	negative	$(n_3\vee n_4)\to n_5$
$n_6$	$\neg n_5$	positive	$n_6\to \neg n_5$
$n_7$	$n_2\wedge n_6$	positive	$n_7,n_7\to (n_2\wedge n_6)$

Convert to CNF clauses:

$$\begin{array}{rl}{n}_1\to \neg q& \equiv \neg n_1\vee \neg q\\ n_2\to (n_1\wedge r)& \equiv (\neg n_2\vee n_1)\wedge (\neg n_2\vee r)\\ (p\leftrightarrow r)\to n_3& \equiv (p\vee r\vee n_3)\wedge (\neg p\vee \neg r\vee n_3)\\ (p\to r)\to n_4& \equiv (p\vee n_4)\wedge (\neg r\vee n_4)\\ (n_3\vee n_4)\to n_5& \equiv (\neg n_3\vee n_5)\wedge (\neg n_4\vee n_5)\\ n_6\to \neg n_5& \equiv \neg n_6\vee \neg n_5\\ n_7& \equiv n_7\\ n_7\to (n_2\wedge n_6)& \equiv (\neg n_7\vee n_2)\wedge (\neg n_7\vee n_6)\end{array}$$

The clausal normal form $C$ is

$$\begin{array}{rl}C=\{& (\neg n_1\vee \neg q),\\ & (\neg n_2\vee n_1),\\ & (\neg n_2\vee r),\\ & (p\vee r\vee n_3),\\ & (\neg p\vee \neg r\vee n_3),\\ & (p\vee n_4),\\ & (\neg r\vee n_4),\\ & (\neg n_3\vee n_5),\\ & (\neg n_4\vee n_5),\\ & (\neg n_6\vee \neg n_5),\\ & (n_7),\\ & (\neg n_7\vee n_2),\\ & (\neg n_7\vee n_6)\}\end{array}$$

(3) Decide the satisfiability of the computed CNF formula $C$ by applying the DPLL method to $C$. If $C$ is satisfiable, give an interpretation which satisfies it.

Select the unit clause $(n_7)$, forcing $n_7\equiv \top$:

$$\begin{array}{rl}{C}_{n_7\equiv \top }=\{& (\neg n_1\vee \neg q),\\ & (\neg n_2\vee n_1),\\ & (\neg n_2\vee r),\\ & (p\vee r\vee n_3),\\ & (\neg p\vee \neg r\vee n_3),\\ & (p\vee n_4),\\ & (\neg r\vee n_4),\\ & (\neg n_3\vee n_5),\\ & (\neg n_4\vee n_5),\\ & (\neg n_6\vee \neg n_5),\\ & \cancel{(n_7)},\\ & (\cancel{\neg n_7\vee }{n}_2),\\ & (\cancel{\neg n_7\vee }{n}_6)\}\end{array}$$

Two new unit clauses appeared, forcing $n_2\equiv n_6\equiv \top$:

$$\begin{array}{rl}{C}_{n_2\equiv \top ,n_6\equiv \top ,n_7\equiv \top }=\{& (\neg n_1\vee \neg q),\\ & (\cancel{\neg n_2\vee }{n}_1),\\ & (\cancel{\neg n_2\vee }r),\\ & (p\vee r\vee n_3),\\ & (\neg p\vee \neg r\vee n_3),\\ & (p\vee n_4),\\ & (\neg r\vee n_4),\\ & (\neg n_3\vee n_5),\\ & (\neg n_4\vee n_5),\\ & (\cancel{\neg n_6\vee }\neg n_5),\\ & (\cancel{n_2}),\\ & (\cancel{n_6})\}\end{array}$$

More unit clauses! Force $n_1\equiv r\equiv \top$, $n_5\equiv \perp$.

$$\begin{array}{rl}{C}_{n_1\equiv \top ,n_2\equiv \top ,n_5\equiv \perp ,n_6\equiv \top ,n_7\equiv \top ,r\equiv \top }=\{& (\cancel{\neg n_1\vee }\neg q),\\ & \cancel{(n_1)},\\ & \cancel{(r)},\\ & \cancel{(p\vee r\vee n_3)},\\ & (\neg p\vee \cancel{\neg r\vee }{n}_3),\\ & (p\vee n_4),\\ & (\cancel{\neg r\vee }{n}_4),\\ & (\neg n_3\cancel{\vee n_5}),\\ & (\neg n_4\cancel{\vee n_5}),\\ & \cancel{(\neg n_5)}\}\end{array}$$

Well… more unit clauses! They force $n_3\equiv n_4\equiv q\equiv \perp$. and $n_4\equiv \top$, i.e., a contradiction.

Therefore, the aforementioned formula is UNSAT.

Problem 2. (20 points)

Problem 2. (20 points)

Formalise the following arguments and verify whether they are correct:

1. I must be punished only if I am guilty; I am guilty. Thus, I must be punished.
2. If I am guilty, I must be punished; I am not guilty. Thus, I must not be punished.

Verifying whether an argument is correct means proving a statement of the following form: from the hypotheses $P_1,\dots ,P_n$, the conclusion $Q$ follows. That is, either formally prove $P_1,\dots ,P_n\models Q$, or exhibit a counterexample to the statement.

Solution

Formalise:

1. $punished\to guilty,guilty\models punished$
2. $guilty\to punished,\neg guilty\models \neg punished$

Consider the first statement. By duality

\begin{align} punished \to guilty, \; guilty &\models punished\\

&\text{iff} \
{punished \to guilty, guilty, \lnot punished} &\text{ is unsat}.

\end{align}

The clause $guilty$ forces $guilty \equiv \top$. [[Knowledge/Equivalent Replacement (Propositional Logic)|Replace]] and simplify the other clauses to

{\lnot punished}.

This set is satisfiable. A [[Knowledge/Countermodel (Propositional Logic)|countermodel]] $I$ is

I = {guilty \mapsto 1, punished \mapsto 0}.

$$Therefore,thefirstentailmentdoesnothold.Considerthesecondstatement.By[[Knowledge/Entailment–UnsatisfiabilityDuality(PropositionalLogic)|duality]]$$

\begin{aligned}
guilty \to punished, \lnot guilty &\models \lnot punished \
\text{iff} \
{guilty \to punished, \lnot guilty, punished} &\text{ is unsat}.
\end{aligned}

The clause $\lnot guilty$ forces $guilty \equiv \bot$. [[Knowledge/Equivalent Replacement (Propositional Logic)|Replace]] and simplify the other clauses to

{ punished }.

There's at least one [[Knowledge/Countermodel (Propositional Logic)|countermodel]]. An example for a [[Knowledge/Countermodel (Propositional Logic)|countermodel]] $I$ is

I = { guilty \mapsto 0, punished \mapsto 1 }.

Problem 3. (20 points)

Problem 3. (20 points)

Let $A$ be a propositional, well-formed formula using $n\ge 1$ propositional variables such that

• $A$ is not a propositional atom; and
• $A$ is built from propositional atoms using only $\neg$ and $\leftrightarrow$.

How many branches does a splitting tree of $A$ have? Provide a sufficiently detailed explanation of your answer.

Solution

Let $b(n)$ denote the number of branches in a splitting tree for $A$.

For $n=1$, splitting on the single propositional variable produces one child for each of its two possible truth values. Since no variables remain, both children simplify to constants. Hence,

$$b(1)=2.$$

Now suppose that $A$ contains $n>1$ propositional variables. Splitting on any variable $p$ produces the two children

$$A_p^{\top }\text{and}{A}_p^{\perp }.$$

Neither $\neg$ nor $\leftrightarrow$ can terminate a branch while another variable remains. In particular,

$$\begin{array}{rlrl}\top \leftrightarrow B& \equiv B,& \perp \leftrightarrow B& \equiv \neg B,\\ B\leftrightarrow \top & \equiv B,& B\leftrightarrow \perp & \equiv \neg B.\end{array}$$

For $n=3$, the repeated binary splitting has the following shape:

Thus, each child still requires splitting on the remaining $n-1$ variables. Both subtrees therefore have $b(n-1)$ branches, giving

$$b(n)=2b(n-1).$$

Together with $b(1)=2$, this yields

$$b(n)=2^n.$$

Therefore, the splitting tree has $2^n$ branches, one for each possible interpretation of its $n$ propositional variables.

Problem 4. (10 points)

Problem 4. (10 points)

Provide either a tableau proof or a counterexample for the statement

$$\neg \exists xA(x)\models \exists x\neg (A(x)\vee A(f(x))).$$

If you provide a counterexample, you have to show that it is in fact a counterexample.

Solution

• $t:\neg \exists xA(x)$ (premise)

• $f:\exists xA(x)$

• $f:A(a)$

• $f:A(f(a))$

• $f:\exists x\neg (A(x)\vee A(f(x))$ (conclusion)

• $f:\neg (A(a)\vee A(f(a))$

• $t:A(a)\vee A(f(a))$

  • (L) Branch
    • $t:A(a)$
      • contradicts $f:A(a)$
      • (L) branch closes
  • (R) Branch
    • $t:A(f(a))$
      • contradicts $f:A(f(a))$
      • (R) branch closes

All branches of the tableau close, i.e., there’s no countermodel for the above statement.

Problem 5. (25 points)

Problem 5. (25 points)

Consider the formula:

$$a=b-4\wedge f(b+1)=c\wedge (f(a+5)\ne c\vee read(write(A,a+2,3),b-3)=1)$$

where $a,b,c$ are integer constants, $f$ is a unary function symbol, $A$ is an array constant, $read$ and $write$ are interpreted in the array theory, and $+,-,1,2,3,\dots$ are interpreted in the standard way over the integers.

Use the Nelson–Oppen decision procedure for reasoning in the combination of the theories of arrays, uninterpreted functions, and linear integer arithmetic. Use the decision procedures for the theory of arrays and the theory of uninterpreted functions, and use simple mathematical reasoning to derive new equalities among the constants in the theory of linear integer arithmetic. If the formula is satisfiable, give an interpretation that satisfies it.

Let $F$ be the formula

$$\begin{array}{rl}F& \equiv \underset{{\phi }_1}{\underbrace{a=b-4}}\wedge \underset{{\phi }_2}{\underbrace{f(b+1)=c}}\wedge (\underset{{\phi }_3}{\underbrace{f(a+5)\ne c}}\vee \underset{{\phi }_4}{\underbrace{read(write(A,a+2,3),b-3)=1}})\\ & \equiv {\phi }_1\wedge {\phi }_2\wedge ({\phi }_3\vee {\phi }_4)\\ & \equiv \underset{F^{(1)}}{\underbrace{({\phi }_1\wedge {\phi }_2\wedge {\phi }_3)}}\vee \underset{F^{(2)}}{\underbrace{({\phi }_1\wedge {\phi }_2\wedge {\phi }_4)}}\\ & \equiv F^{(1)}\vee F^{(2)}.\end{array}$$

Consider $F^{(1)}$ first.

Theory of linear integer arithmetic (${\mathcal{T}}_{\mathbb{Z}}$):

$$\begin{array}{rl}a& =b-4\\ {\ell }_1& =b+1\\ {\ell }_2& =a+5\end{array}$$

Theory of equality with uninterpreted functions (${\mathcal{T}}_{\text{UE}}$):

$$\begin{array}{rl}f({\ell }_1)& =c\\ f({\ell }_2)& \ne c\end{array}$$

${\mathcal{T}}_{\mathbb{Z}}$ emits

$$\begin{array}{rl}a=b-4,{\ell }_2=a+5& \to {\ell }_2=b-4+5\\ & \to {\ell }_2=b+1\\ & \\ {\ell }_2=b+1,{\ell }_1=b+1& \to \underline{{\ell }_2={\ell }_1}.\end{array}$$

Propagate ${\ell }_2={\ell }_1$.

Theory of linear integer arithmetic (${\mathcal{T}}_{\mathbb{Z}}$):

$$\begin{array}{rl}a& =b-4\\ {\ell }_1& =b+1\\ {\ell }_2& =a+5\\ {\ell }_2& ={\ell }_1\end{array}$$

Theory of equality with uninterpreted functions (${\mathcal{T}}_{\text{UE}}$):

$$\begin{array}{rl}f({\ell }_1)& =c\\ f({\ell }_2)& \ne c\\ {\ell }_2& ={\ell }_1\end{array}$$

${\mathcal{T}}_{\text{UE}}$ infers

$$\begin{array}{rl}{\ell }_2={\ell }_1& \to f({\ell }_2)=f({\ell }_1)\\ & \\ f({\ell }_2)\ne c,f({\ell }_2)=f({\ell }_1)& \to f({\ell }_1)\ne c\end{array}$$

But $f({\ell }_1)=c$ according to the theory’s fragments. Contradiction. Hence, $F^{(1)}$ is UNSAT.

Consider $F^{(2)}$.

Theory of linear integer arithmetic (${\mathcal{T}}_{\mathbb{Z}}$):

$$\begin{array}{rl}a& =b-4\\ {\ell }_1& =b+1\\ {\ell }_2& =a+2\\ {\ell }_3& =3\\ {\ell }_4& =b-3\\ {\ell }_5& =1\end{array}$$

Theory of equality with uninterpreted functions (${\mathcal{T}}_{\text{UE}}$):

$$\begin{array}{rl}f({\ell }_1)& =c\end{array}$$

Theory of arrays (${\mathcal{T}}_A$):

$$\begin{array}{r}read(write(A,{\ell }_2,{\ell }_3),{\ell }_4)={\ell }_5\end{array}$$

${\mathcal{T}}_A$ infers

$${\ell }_5=read(write(A,{\ell }_2,{\ell }_3),{\ell }_4)\to ({\ell }_2={\ell }_4\wedge {\ell }_5={\ell }_3)\vee ({\ell }_2\ne {\ell }_4\wedge {\ell }_5=read(A,{\ell }_4))$$

Given that ${\ell }_3=3$ and ${\ell }_5=1$, i.e., ${\ell }_3\ne {\ell }_5$ (under the standard interpretation over integers), the left branch cannot be true. Propagate the latter branch.

Theory of linear integer arithmetic (${\mathcal{T}}_{\mathbb{Z}}$):

$$\begin{array}{rl}a& =b-4\\ {\ell }_1& =b+1\\ {\ell }_2& =a+2\\ {\ell }_3& =3\\ {\ell }_4& =b-3\\ {\ell }_5& =1\\ {\ell }_2& \ne {\ell }_4\end{array}$$

Theory of equality with uninterpreted functions (${\mathcal{T}}_{\text{UE}}$):

$$\begin{array}{rl}f({\ell }_1)& =c\end{array}$$

Theory of arrays (${\mathcal{T}}_A$):

$$\begin{array}{rl}read(write(A,{\ell }_2,{\ell }_3),{\ell }_4)={\ell }_5& \\ {\ell }_2\ne {\ell }_4& \\ read(A,{\ell }_4)& ={\ell }_5\end{array}$$ $$\begin{array}{rl}{a}^I& =0\\ b^I& =4\\ {\ell }_1^I& =5\\ {\ell }_2^I& =2\\ {\ell }_3^I& =3\\ {\ell }_4^I& =1\\ {\ell }_5^I& =1\\ c^I& =420\\ f^I& =\{5\mapsto 420\}\\ & \\ {\alpha }^I& =\mathbb{Z}\end{array}$$

with sort $\alpha$ for $a,b,c,{\ell }_1,{\ell }_2,\ell ,{\ell }_3,{\ell }_4,{\ell }_5:\alpha$ and $f:\alpha \to \alpha$.