LARA

e

Deriving Propositional Resolution

We are extending the notion of substitution on formulas to sets of formulas by

\begin{equation*} subst(\sigma,S) = \{ subst(\sigma,F) \mid F \in S \} \end{equation*}

To make intuition clearer, we will next use quantification over potentially infinitely many variables and conjunctions over infinitely many formulas.

Proof System Based on Projecting Variables

We first derive a more abstract proof system and that show that resolution is a special case of it.

Key Idea

The condition that $S$ is satisfiable is equivalent to the truth of

\begin{equation*} \exists p_1,p_2,p_3,\ldots.\ \bigwedge_{F \in S} F \end{equation*}

which, by changing the order of quantifiers, is:

\begin{equation*} \exists p_2,p_3,\ldots.\ \exists p_1. \bigwedge_{F \in S} F \end{equation*}

By expanding existential quantifier, $\exists p_1. \bigwedge_{F \in S} F$ is eqivalent to

\begin{equation*} ((\bigwedge_{F \in S} subst(p_1 \mapsto {\it false},F)) \lor (\bigwedge_{F \in S} subst(p_1 \mapsto {\it true},F)) \end{equation*}

which, by distributivity of $\lor$ through $\land$ is:

\begin{equation*} \bigwedge_{F_1,F_2 \in S} (subst(p_1 \mapsto {\it false},F_1) \lor subst(p_1 \mapsto {\it true},F_2)) \end{equation*}

Let

\begin{equation*} ProjectForm(F_1,F_2,p) = (subst(p \mapsto {\it false},F_1) \lor (subst(p \mapsto {\it true},F_2)) \end{equation*}

Then we conclude that $\exists p. S$ is equivalent to $ProjectSet(S,p)$ defined by

\begin{equation*} ProjectSet(S,p) = \{ ProjectForm(F_1,F_2,p) \mid F_1,F_2 \in S \} \end{equation*}

Projection Proof Rules

Above we justified the use of $ProjectForm(F_1,F_2,p)$ as an inference rule. We write such rule:

\begin{equation*} \frac{F_1 \; \ F_2} {(subst(p \mapsto {\it false},F_1) \lor (subst(p \mapsto {\it true},F_2))} \end{equation*}

The soundness of projection rule follows from the fact that for every interpretation $I$, if $I \models S$, then also $I \models ProjectSet(S,p)$.

Applying the projection rule we obtain formulas with fewer and fewer variables. We therefore also add the “ground contradiction rule”

\begin{equation*} \frac{F} {{\it false}} \end{equation*}

where $F$ is formula that has no variables and that evaluates to false (ground contradictory formula). This rule is trivially sound: we can never have a model of a ground formula that evaluates to false.

Iterating Rule Application

Given some enumeration $p_1,p_2,\ldots$ of propositional variables in $S$, we define the notion of applying projection along all propositional variables, denoted $P^*$:

\begin{equation*}\begin{array}{l} P_0(S) = S \\ P_{n+1}(S) = ProjectSet(P_n(S),p_{n+1}) \\ P^*(S) = \bigcup_{n \geq 0} P_n(S) \end{array}\end{equation*}

Completeness of Projection Rules

We wish to show that projection rules are a sound and complete approach for checking satisfiability of finite and infinite sets formulas. More precisely:

  • if we can derive false from $S$ using projection rules and the ground rule, then $S$ is unsatisfiable
  • if $S$ is unsatisfiable, then we can derive false using projection rules and one application of the ground rule

Because we can derive false precisely when we have a ground false formula, these statements become:

  • if $P^*(S)$ contains a ground contradiction, then $S$ is not satisfiable
  • if $S$ is not satisfiable then $P^k(S)$ contains a ground contradiction for some natural number $k$.

The first statement follows from soundness of projection rules. We next prove the second statement.

Suppose that $S$ is not satisfiable. By the Compactness Theorem, a finite subset $T = \{F_1,\ldots,F_n\}$ is not satisfiable. Let $FV(F_1) \cup \ldots \cup FV(F_n) \subseteq \{p_1,\ldots,p_M\}$.

Consider the set

\begin{equation*} A = \bigcup_{i=1}^M P_i(S) \end{equation*}

By definition of $P_i$, we can show that $A$ contains a subset $A_0$ of ground propositional formulas equivalent to

\begin{equation*} \exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n) \end{equation*}

Because the above formula is contradictory, $A_0$ is a contradictory set of ground propositional formulas, so it contains a ground contradiction. Thus, we can set $k=M$ in the above theorem.

Improvement: Subsumption Rules

Note also that if $\models (F \rightarrow G)$, where $F$ has been derived before, and $FV(G) \subseteq FV(F)$, then deriving $G$ does not help derive a ground contradiction, because the contradiction would also be derived using $F$. If we derive such formula, we can immediately delete it so that it does not slow us down.

In particular, a ground true formula can be deleted.

Resolution as Projection

Recall Definition of Propositional Resolution.

Instead of arbitrary formulas, use clauses as sets of literals. The projection rule becomes

\begin{equation*} \frac{C_1 \; \ C_2} {(subst(p \mapsto {\it false},C_1) \cup (subst(p \mapsto {\it true},C_2))} \end{equation*}

If $C$ is a clause, then

\begin{equation*} subst(\{p \mapsto {\it false}\},C) \end{equation*}

is equivalent to

There are several cases:

  • if $p \notin C_1$ then
  • if $\lnot p \notin C_2$ then
  • if $p \in C_1$ and $(\lnot p) \in C_2$, then

Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule.