Propositional Resolution Calculus

propositional-logic

Definition

Propositional Resolution Calculus

The propositional resolution calculus is a calculus for sets of clauses. Its derivations use the resolution inference rule and the factoring inference rule.

A derivation that derives the empty clause $\square$ is a refutation.

Inference Rules

Resolution

Definition

Resolution Inference Rule (Propositional Resolution)

$${\frac{C\vee p\neg p\vee D}{C\vee D}}_{(\text{resolution})}$$

where $C\vee D$ is called the the resolvent and $p$ is called resolved atom.

Link to original

Factoring

Definition

Propositional Factoring Inference Rule

$${\frac{C\vee F\vee F}{C\vee F}}_{(\text{factoring})}$$

where $C\vee F$ is called factor.

Link to original

Derivation

Definition

Derivation (Propositional Resolution)

In the propositional resolution calculus, a derivation from a set of clauses $KB$ is a sequence of clauses that starts with the input clauses and then adds clauses obtained by allowed inference steps.

If

$$KB=\{C_1,\dots ,C_k\},$$

then a derivation from $KB$ has the form

$$C_1,\dots ,C_k,C_{k+1},\dots ,C_n,\dots$$

where $C_1,\dots ,C_k$ are the input clauses, and every derived clause $C_n$ with $n\ge k+1$ is either:

• a resolvent of earlier clauses $C_i$ and $C_j$, for some $1\le i,j<n$; or
• a factor of an earlier clause $C_i$, using the factoring inference rule, for some $1\le i<n$.

A derivation is a refutation when one of its derived clauses is the empty clause $\square$.

Link to original

Refutation

Definition

Refutation (Propositional Resolution)

A refutation of a set of clauses $KB$ is a derivation from $KB$ that derives the empty clause $\square$.

Since $\square$ is unsatisfiable, a refutation proves that $KB$ is unsatisfiable. In proof by refutation, this is used to prove an entailment by deriving $\square$ from $KB\cup \{\neg A\}$.

Link to original

Algorithm

Definition

Resolution Algorithm

The resolution algorithm decides whether a set of formulas $KB=\{Q_1,\dots ,Q_n\}$ entails a formula $P$ by applying the propositional resolution calculus to

$$Q_1\wedge \cdots \wedge Q_n\wedge \neg P.$$

By the entailment–unsatisfiability duality, $KB\models P$ holds exactly when this formula is unsatisfiable.

Link to original

Soundness

Soundness

The propositional resolution calculus is sound: if there is a refutation of $KB$, then $KB$ is unsatisfiable.

Equivalently, if $KB$ is satisfiable, then no derivation from $KB$ can contain the empty clause $\square$.

$I$ be an interpretation satisfying all input clauses in $KB$. We show that each inference rule preserves truth under $I$.

For resolution, assume

$$I(C\vee p)=1\text{and}I(\neg p\vee D)=1.$$

If $I(p)=0$, then the first premise forces $I(C)=1$. If $I(p)=1$, then the second premise forces $I(D)=1$. In both cases,

$$I(C\vee D)=1.$$

For factoring, the clauses $C\vee F\vee F$ and $C\vee F$ have the same truth value under every interpretation. Hence

$$I(C\vee F\vee F)=1⟹I(C\vee F)=1.$$

Therefore, by induction over the derivation, every derived clause is true under $I$.
But $I(\square )=0$ for every interpretation $I$.
Hence a satisfiable $KB$ cannot have a derivation containing $\square$.
By contraposition, if a refutation of $KB$ exists, then $KB$ is unsatisfiable.

Completeness

Refutational Completeness

The propositional resolution calculus is refutationally complete: if a finite set of clauses $S$ is unsatisfiable, then

$$S⊢\square .$$

$S$ under resolution and factoring: repeatedly add every clause obtainable by these rules until no new clause can be added. This process terminates because only finitely many clauses can be built from the finitely many atoms occurring in $S$.

Let $S^{\ast }$ be the saturated set. It is enough to show that if $\square \notin S^{\ast }$, then $S^{\ast }$ is satisfiable. Since $S\subseteq S^{\ast }$, this would make $S$ satisfiable too, contradicting the assumption.

We prove the claim by induction on the number of atoms in $S^{\ast }$.

If there are no atoms, the only possible unsatisfied clause is $\square$. Since $\square \notin S^{\ast }$, the set is satisfiable.

For the induction step, choose an atom $p$. Define the two simplified clause sets

$$\begin{array}{rl}{S}_p^{\ast }& =\{C\setminus \{\neg p\}\mid C\in S^{\ast },p\notin C\},\\ S_{\neg p}^{\ast }& =\{C\setminus \{p\}\mid C\in S^{\ast },\neg p\notin C\}.\end{array}$$

The set $S_p^{\ast }$ is the result of setting $p$ to true: clauses containing $p$ are already satisfied, and occurrences of $\neg p$ are deleted. The set $S_{\neg p}^{\ast }$ is defined symmetrically for setting $p$ to false.

These simplified sets are again saturated under resolution and factoring on the remaining atoms. If both contained $\square$, then $S^{\ast }$ would contain both unit clauses $\neg p$ and $p$, so one further resolution step would derive $\square$, contradicting $\square \notin S^{\ast }$.

Hence at least one of $S_p^{\ast }$ and $S_{\neg p}^{\ast }$ does not contain $\square$. By the induction hypothesis, that simplified set is satisfiable. Extend its satisfying interpretation by setting $p$ accordingly. This gives a satisfying interpretation of $S^{\ast }$.

Therefore every saturated clause set without $\square$ is satisfiable. Since $S$ was assumed unsatisfiable, the saturation $S^{\ast }$ must contain $\square$. The sequence of saturation steps that first produces $\square$ is a refutation of $S$.