# Logic for Computer Scientists/Propositional Logic/Resolution

## Resolution

In this subsection we will develop a calculus for propositional logic. Until now we have a language, i.e. a set of formulae and we have investigated into semantics and some properties of formulae or sets of clauses. Now we will introduce an inference rule, namely the resolution rule, which allows to derive new clauses from given ones.

## Definition 10

A clause ${\displaystyle R}$ is a resolvent of clauses ${\displaystyle C_{1}}$ and ${\displaystyle C_{2}}$, if there is a literal ${\displaystyle L\in C_{1}}$ and ${\displaystyle {\overline {L}}\in C_{2}}$ and

${\displaystyle R=(C_{1}-\{L\})\cup (C_{2}-\{{\overline {L}}\})}$

where ${\displaystyle {\overline {L}}={\begin{cases}\;\;\,\lnot A\;{\text{ if }}L=A\\\;\;\,A\;{\text{ if }}L=\lnot A\end{cases}}}$

Note that there is a special case, if we construct the resolvent out of two literals, i.e. ${\displaystyle L}$ and ${\displaystyle {\overline {L}}}$ can be resolved upon and yield the empty set. This empty resolvent is depicted by the special symbol ${\displaystyle \square }$.
${\displaystyle \square }$ denotes an unsatisfiable formula. We define a clause set, which contains this empty clause to be unsatisfiable,

In the following we investigate in properties of the resolution rule and the entire calculus. The following Lemma is stating the correctness of one single application of the resolution rule.

## Theorem 7

If ${\displaystyle S}$ is a set of clauses and ${\displaystyle R}$ a resolvent of ${\displaystyle C_{1},C_{2}\in S}$, then ${\displaystyle S\equiv S\cup \{R\}}$

Proof: Let ${\displaystyle {\mathcal {A}}}$ be an assignment for ${\displaystyle S}$; hence it is an assignment for ${\displaystyle S\equiv S\cup \{R\}}$ as well. Assume ${\displaystyle {\mathcal {A}}\models S}$: hence for all clauses ${\displaystyle C}$ from ${\displaystyle S}$, we have that ${\displaystyle {\mathcal {A}}\models C}$. The resolvent ${\displaystyle R}$ of ${\displaystyle C_{1}}$ and ${\displaystyle C_{2}}$ looks like:

${\displaystyle R=(C_{1}-\{L\})\cup (C_{2}-\{{\overline {L}}\})}$

where ${\displaystyle L\in C_{1}}$ and ${\displaystyle {\overline {L}}\in C_{2}}$. Now there are two cases:

• ${\displaystyle {\mathcal {A}}\models L}$: From ${\displaystyle {\mathcal {A}}\models C_{2}}$ and ${\displaystyle {\mathcal {A}}\not \models {\overline {L}}}$, we conclude ${\displaystyle {\mathcal {A}}\models (C_{2}-\{{\overline {L}}\})}$ and hence ${\displaystyle {\mathcal {A}}\models R}$.
• ${\displaystyle {\mathcal {A}}\not \models L}$: From ${\displaystyle {\mathcal {A}}\models C_{1}}$ we conclude ${\displaystyle {\mathcal {A}}\models (C_{1}-\{L\})}$ and hence ${\displaystyle {\mathcal {A}}\models R}$. The opposite direction of the lemma is obvious.

## Definition 11

Let ${\displaystyle S}$ be s set of clauses and

${\displaystyle Res(S)=S\cup \{R\mid R{\text{ is a resolvent of two clauses in }}S\}}$

then

${\displaystyle Res^{0}(S)=S}$
${\displaystyle Res^{n+1}(S)=Res(Res^{n}(S)),n\geq 0}$
${\displaystyle Res^{*}(S)=\bigcup _{n\geq 0}Res^{n}(S)}$

If we understand the process of iterating the Res-operator as a procedure for deriving new clauses from a given set, and in particular to derive possibly the empty clause, we have to ask, under which circumstances we get the empty clause, and vice versa, what does it mean if we get it. These properties are investigates in the following two Theorems.

## Theorem 8 (Correctness)

Let ${\displaystyle S}$ be a set of clauses. If ${\displaystyle \square \in Res^{*}(S)}$ then ${\displaystyle S}$ is unsatisfiable.

Proof: From ${\displaystyle \square \in Res^{*}(S)}$ we conclude, that ${\displaystyle \square }$ is obtained by resolution from two clauses ${\displaystyle C_{1}=\{L\}}$ and ${\displaystyle C_{2}=\{{\overline {L}}\}}$. Hence there is a ${\displaystyle \exists n\geq 0}$ such that ${\displaystyle \square \in Res^{n}(S)}$ and ${\displaystyle C_{1},C_{2}\in Res^{n}(S)}$ and therefore ${\displaystyle Res^{n}(S)}$ is unsatisfiable. From Theorem (resolution-lemma) we conclude that ${\displaystyle Res^{n}(S)\equiv S}$ and hence ${\displaystyle S}$ is unsatisfiable.

## Theorem 9 (Completeness)

Let ${\displaystyle S}$ be a finite set of clauses. If ${\displaystyle S}$ is unsatisfiable then ${\displaystyle \square \in Res^{*}(S)}$.

Proof: Induction over the number ${\displaystyle n}$ of atomic formulae in ${\displaystyle S}$. With ${\displaystyle n=0}$ we have ${\displaystyle S=\{\square \}}$and hence ${\displaystyle \square \in S\subseteq Res^{*}(S)}$.

Assume ${\displaystyle n}$ fixed and for every unsatisfiable set of clauses ${\displaystyle S}$ with ${\displaystyle n}$ atomic formulae ${\displaystyle A_{1},\cdots ,A_{n}}$ it holds that ${\displaystyle \square \in Res^{*}(S)}$.

Assume a set of clauses ${\displaystyle S}$ with atomic formulae ${\displaystyle A_{1},\cdots ,A_{n},A_{n+1}}$. In the following we construct two clause sets ${\displaystyle S_{f}}$ and ${\displaystyle S_{t}}$:

• ${\displaystyle S_{f}}$ is received from ${\displaystyle S}$ by deleting every occurrence of ${\displaystyle A_{n+1}}$ in a clause and by deleting every clause which contains an occurrence of ${\displaystyle \lnot A_{n+1}}$. This transformation obviously corresponds to interpreting the atom ${\displaystyle A_{n+1}}$ with ${\displaystyle false}$,
• ${\displaystyle S_{t}}$ results from a similar transformation, where occurrences of ${\displaystyle \lnot A_{n+1}}$ and clauses containing ${\displaystyle A_{n+1}}$ are deleted, hence ${\displaystyle A_{n+1}}$ is interpreted with ${\displaystyle true}$.

Let us show, that both ${\displaystyle S_{f}}$ and ${\displaystyle S_{t}}$ are unsatisfiable: Assume an assignment ${\displaystyle {\mathcal {A}}}$ for the atomic formale ${\displaystyle \{A_{1},\cdots ,A_{n}\}}$ which is a model for ${\displaystyle S_{f}}$. Hence the assignment ${\displaystyle {\mathcal {A}}'(B)={\begin{cases}\;\;\,{\mathcal {A}}(B)\;{\text{ if }}B\in \{A_{1},\cdots ,A_{n}\}\\\;\;\,false{\text{ if }}B=A_{n+1}\end{cases}}}$ is a model for ${\displaystyle S}$, which leads to a contradiction. A similar construction shows that ${\displaystyle S_{t}}$ is unsatisfiable. Hence then we can use the induction assumption to conclude that ${\displaystyle \square \in Res^{*}(S_{t})}$ and ${\displaystyle \square \in Res^{*}(S_{f})}$. Hence there is a sequence of clauses

${\displaystyle C_{1},\cdots ,C_{m}=\square }$

such that ${\displaystyle \forall 1\leq i\leq m}$ it holds ${\displaystyle C_{i}\in S_{f}}$ or ${\displaystyle C_{i}}$ is a resolvent of two clauses ${\displaystyle C_{a}}$ and ${\displaystyle C_{b}}$ with ${\displaystyle a,b.There is an analog sequence for ${\displaystyle S_{t}}$:

${\displaystyle C_{1}',\cdots ,C_{t}'=\square }$

Now we are going to reintroduce the previously deleted literals ${\displaystyle A_{n+1}}$ and ${\displaystyle \lnot A_{n+1}}$ in the two sequences:

• Clause ${\displaystyle C_{i}}$ which has been the result of deleting ${\displaystyle A_{n+1}}$ from the original clause in ${\displaystyle S}$ are again modified to ${\displaystyle C_{i}\cup \{A_{n}+1\}}$. This results in a sequence
${\displaystyle {\overline {C_{1}}},\cdots ,{\overline {C_{m}}}}$

where ${\displaystyle {\overline {C_{m}}}}$ is either ${\displaystyle \square }$ or ${\displaystyle A_{n+1}}$.

• Analogous we introduce ${\displaystyle \lnot A_{n+1}}$ in the second sequence, such that ${\displaystyle {\overline {C_{t}'}}}$ is either ${\displaystyle \square }$ or ${\displaystyle \lnot A_{n+1}}$

In any of the above cases we get ${\displaystyle \square \in Res^{*}(S)}$ latest after one resolution step with ${\displaystyle {\overline {C_{m}}}}$ and ${\displaystyle {\overline {C_{t}'}}}$.

Based on the theorems for correctness and completeness, we give a procedure for deciding the satisfiability of propositional formulae.

 Deciding Satisfiability of Propositional Formulae Given a propositional formula ${\displaystyle F}$. Transform ${\displaystyle F}$ into an equivalent CNF ${\displaystyle S}$. Compute ${\displaystyle Res^{n}(S)}$ for ${\displaystyle n=0,1,2,\cdots }$ If ${\displaystyle \square \in Res^{n}(S)}$ then Stop: unsatisfiable . if ${\displaystyle Res^{n}(S)=Res^{n+1}(S)}$ then Stop: satisfiable .

## Theorem 10

If ${\displaystyle S}$ is a finite set of clauses, then there exists a ${\displaystyle k\geq 0}$ such that

${\displaystyle Res^{k}(S)=Res^{k+1}(S)}$

Until now, we have been dealing with sets of clauses. In the following it will turn out, that it is helpful to talk about sequences of applications of the resolution rule.

## Definition 12

A deduction of a clause ${\displaystyle C}$ from a set of clauses ${\displaystyle S}$ is a sequence ${\displaystyle C_{1},\cdots ,C_{n}}$, such that

• ${\displaystyle C_{n}=C}$ and
• ${\displaystyle \forall 1\leq i\leq n:(C_{i}\in S{\text{ or }}\exists l,r

A deduction of the empty clause ${\displaystyle \square }$ from ${\displaystyle S}$ is called a refutation of ${\displaystyle S}$.

Example We want to show, that the formula ${\displaystyle K=((B\land \lnot A)\lor C)}$ is a logical consequence of ${\displaystyle F=((A\lor (B\lor C))\land (C\lor \lnot A))}$. For this negate ${\displaystyle K}$ and prove the unsatisfiability of ${\displaystyle F\land \lnot K}$

For this you can use the interaction in this book in various forms:

• Use the interaction Truth Tables for proving the unsatisfiability, or
• use the interaction CNF Transformation for transforming the formula into CNF, and then
• use the following interaction Resolution.

## Problems

#### Problem 23 (Propositional)

Compute ${\displaystyle Res^{n}(M)}$ for all ${\displaystyle n\geq 0}$ and ${\displaystyle Res^{*}(M)}$ for the following set of clauses:

1. ${\displaystyle M=\{\{A\},\{B\},\{\lnot A,C\},\{B,\lnot C,\lnot D\},\{\lnot C,D\},\{\lnot D\}}$
2. ${\displaystyle M=\{\{A,\lnot B\},\{A,B\},\{\lnot A\}\}}$
3. ${\displaystyle M=\{\{A,B,C\},\{\lnot B,\lnot C\},\{\lnot A,C\}\}}$
4. ${\displaystyle M=\{\{\lnot A,\lnot B\},\{B,C\},\{\lnot C,A\}\}}$

Which formula is satisfiable or which is unsatisfiable?
${\displaystyle \Box }$

#### Problem 24 (Propositional)

Indicate all resolvent of the clauses in S, where ${\displaystyle S=\{\{A,\lnot B,C\},\{A,B,E\},\{\lnot A,C,\lnot D\},\{A,\lnot E\}\}}$
${\displaystyle \Box }$

#### Problem 25 (Propositional)

Prove: A resolvent ${\displaystyle R}$ of two clauses ${\displaystyle C_{1}}$ and ${\displaystyle C_{2}}$ is a logical consequence from ${\displaystyle C_{1}}$ and ${\displaystyle C_{2}}$. Note: Use the definition of "consequence".
${\displaystyle \Box }$

#### Problem 26 (Propositional)

Let ${\displaystyle M}$ be a set of formulae and ${\displaystyle F}$ a formula. Prove:

${\displaystyle M\models F}$ iff ${\displaystyle M\cup \{\lnot F\}}$ is unsatisfiable.

${\displaystyle \Box }$

#### Problem 27 (Propositional)

Compute ${\displaystyle Res^{n}(S)}$ with ${\displaystyle n=0,1,2}$ and

${\displaystyle S=\{\{A,\lnot B,C\},\{B,C\},A\{\lnot ,C\},\{B,\lnot C\},\{\lnot C\}\}}$
${\displaystyle \Box }$

#### Problem 28 (Propositional)

Show that the following set ${\displaystyle S}$ of formulae is unsatisfiable, by giving a refutation.
${\displaystyle S=(B\lor C\lor D)\land (\lnot C)\land (\lnot B\lor C)\land (B\lor \lnot D)}$
${\displaystyle \Box }$

#### Problem 29 (Propositional)

Show by using the resolution rule, that ${\displaystyle \lnot A\land \lnot B\land C}$ is an inference from the set of clauses ${\displaystyle F=\{\{A,C\},\{\lnot B,\lnot C\},\{\lnot A\}\}}$.
${\displaystyle \Box }$

#### Problem 30 (Propositional)

Show by using the resolution rule, that ${\displaystyle ((P\to Q{\text{ is }})\land P)\to Q}$ is a tautology.
${\displaystyle \Box }$