Lab for Automated Reasoning and Analysis LARA


Deriving Propositional Resolution

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 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

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

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

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

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

\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.

sav12/deriving_propositional_resolution.txt · Last modified: 2015/04/21 17:33 (external edit)
© EPFL 2018 - Legal notice