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

    subst(\sigma,S) = \{ subst(\sigma,F) \mid F \in S \}

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

  \exists p_1,p_2,p_3,\ldots.\ \bigwedge_{F \in S} F

which, by changing the order of quantifiers, is:

  \exists p_2,p_3,\ldots.\ \exists p_1. \bigwedge_{F \in S} F

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

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

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

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


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

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

   ProjectSet(S,p) = \{ ProjectForm(F_1,F_2,p) \mid F_1,F_2 \in S \}

Projection Proof Rules

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

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

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”

{{\it false}}

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^*$:

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

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

    A = \bigcup_{i=1}^M P_i(S)

By definition of $P_i$, we can show that the set $A$ contains the conjunctive normal form of the expansion of

    \exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)

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

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

If $C$ is a clause, then

   subst(\{p \mapsto {\it false}\},C)

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.