LARA

Deriving Propositional Resolution

We next consider proof rules for checking Satisfiability of Sets of Formulas.

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, then $S$ is unsatisfiable
  • if $S$ is unsatisfiable, then we can derive false using projection rules

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

  • if ${\it false} \in P^*(S)$ then $S$ is not satisfiable
  • if $S$ is not satisfiable then ${\it false} \in P^*(S)$

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

Suppose that it ${\it false} \notin P^*(S)$. We claim that $S$ is satisfiable. We show that every finite set is satisfiable, so the property will follow from the Compactness Theorem.

Consider any finite $T \subseteq S$. We show that $T$ it is satisfiable. Let $T = \{F_1,\ldots,F_n\}$ and 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 the set $A$ contains the conjunctive normal form of the expansion of

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

Each of these conjuncts is a ground formula (all variables $p_1,\ldots,p_M$ have been instantiated), so the formula evaluates to either true or false. By assumption, $P^*(S)$ and therefore $A$ do not contain a ground contradiction. Therefore, each conjunct of $\exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)$ is true and $T$ is satisfiable.

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.