This is an old revision of the document!
Deriving Propositional Resolution
We next consider proof rules for checking Satisfiability of Sets of Formulas.
We 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 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, 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 through
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))
\] Let \[
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 is equivalent to
defined by
\[
Proj(S,p) = \{ ProjectForm(F_1,F_2,p) \mid F_1,F_2 \in S \}
\]
Projection Proof Rules
Th justified the use of 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 , if
, then also
.
Applying the projection rule we obtain formulas with fewer and fewer variables. We therefore also add the “ground contradiction rule”
\[
\frac{F}
it_false
\]
where is formula that has no variables and that evaluates to false (ground contradictory formula). This rule is trivially sound.
Iterating Rule Application
Given some enumeration of propositional variables in
, we define the notion of applying projection along all propositional variables, denoted
:
\[\begin{array}{l}
P_0(S) = S \\ P_{n+1}(S) = Proj(P_n(S),p_{n+1}) \\ P^*(S) = \bigcup_{n \geq 0} P_n(S)
\end{array}\]
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
using projection rules, then
is unsatisfiable
- if
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
then
is not satisfiable
- if
is not satisfiable then
The first statement follows from soundness of projection rules. We next prove the second statement.
Suppose that it . We claim that
is satisfiable. We show that every finite set is satisfiable, so the property follows from the Compactness Theorem.
Consider any finite . We show that
it is satisfiable. Let
and let
. Consider the set
\[
A = \bigcup_{i=1}^M P_i(S)
\]
By definition of , we can show that the set
contains the expansion of
\[
\exists p_1,\ldots,p_M. (F_1 \land \ldots \land F_n)
\]
This expansion is a ground formula, so it evaluates to either true or false. By assumption, and therefore
do not contain ground contradiction. Therefore,
is true and
is satisfiable.
Improvement: Simplification Rules
Of course, we do not need to wait until we reach a ground contradiction. Whenever we substitute variable with true or false, we can immediately simplify the formula using sound simplification rules.
When we introduce simplifications we still manipulate equivalent formulas, so soundness and completeness remain the same.
Improvement: Subsumption Rules
Note also that if , where
has been derived before, and
, then deriving
does not help derive a ground contradiction, because the contradiction would also be derived using
. 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 is a clause, then
\[
subst(\{p \mapsto {\it false}\},C)
\]
There are several cases:
Therefore, for clauses, projection (with some elimination of redundant conclusions) is exactly the resolution proof rule.