Is propositional resolution a complete proof system?

Question

This question is about propositional logic and all occurrences of "resolution" should be read as "propositional resolution".

This question is something extremely basic but it has been bothering me for a while. I see people assert that propositional resolution is complete but I also see people assert that resolution is incomplete. I understand the sense in which resolution is incomplete. I also see why people might claim it is complete but the word "complete" differs from the way "complete" is used when describing natural deduction or the sequent calculus. Even the qualifier "refutation complete" does not help because the formulae have to be in CNF and the transformation of a formula to an equivalent CNF formula or equisatisfiable CNF formula via the Tseitin transformation is not accounted for within the proof system.

Soundness and Completeness

Let us assume the setting of classical propositional logic with a relation $\models$ between some universe of structures and a set of formulae and the classical Tarskian notion of truth in a structure. We write $\models \varphi$ if $\varphi$ is true in all structures being considered. I will also assume a system $\vdash$ for deriving formulae from formulae.

The system $\vdash$ is sound with respect to $\models$ if whenever we have $\vdash \varphi$, we also have $\models \varphi$. The system $\vdash$ is complete with respect to $\models$ if whenever we have $\models \varphi$, we also have $\vdash \varphi$.

The Resolution Rule

A literal is an atomic proposition or its negation. A clause is a disjunction of literals. A formula in CNF is a conjunction of clauses. The resolution rule asserts that

The resolution rule asserts that if the conjunction of the clause $C \lor p$ with the clause $\neg p \lor D$ is satisfiable, the clause $C \lor D$ must also be satisfiable.

I am not sure if the resolution rule alone can be understood as a proof system because there are no rules for introduction of formulae. I assume we at least need a hypothesis rule that allows introduction of clauses.

Incompleteness of resolution

It is known that resolution is a sound proof system. Meaning, if we can derive a clause $C$ from a formula $F$ using resolution then $\models F \implies C$. Resolution is also refutation complete meaning if we have $\models F \implies \bot$ then we can derive $\bot$ from $F$ using resolution.

Consider the formule

$\varphi := p \land q$ and $\psi := p \lor q$.

In Gentzen's system LK or using natural deduction, I can derive the implication $\varphi \implies \psi$ entirely within the proof system. I cannot derive this implication using resolution because if I start with $\varphi$, there are no resolvents.

I see how I can prove the validity of this implication using resolution:

1. Consider the formula $\neg (\varphi \implies \psi)$
2. Turn the formula above into CNF either using standard distributivity rules or using the Tseitin transformation
3. Derive $\bot$ from the transformed formula using resolution.

This approach is unsatisfying to me because it requires me to perform steps (1) and (2) which are outside the resolution proof system. So it seems there is a very clear sense in which resolution is not complete the way we say that natural deduction or sequent calculi are complete.

Questions

Given all that above, my questions are:

1. What proof system is being considered when discussing resolution? Is it just the resolution rule? What are the other rules?
2. It seems very clear to me that resolution is not complete in the sense that natural deduction and sequent calculi are complete. Does the literature asserting that resolution is complete abuse terminology just because the sense in which resolution is complete is more interesting than the sense in which it is incomplete?
3. Has this difference in notions of completeness as applied to resolution and elsewhere and how to reconcile them been discussed at greater depth in the literature?
4. I realise also that resolution can be formulated within sequent calculi in terms of the cut rule. Is the "right" proof theoretic view of resolution just that it is a fragment of the sequent calculus that suffices for checking satisfiability of formulae in CNF?

Answer 1

What proof system is being considered when discussing resolution? Is it just the resolution rule? What are the other rules?

I discuss resolution in the context of "clauses", which are sequents made up of only literals. A classical clause would look like $$A_1,\ldots,A_n \to B_1,\ldots,B_m$$ But we can also write it as $${} \to \bar{A}_1,\ldots,\bar{A}_n, B_1, \ldots, B_m$$ and work with just one sided sequents. It is conventional to treat these one-sided sequents as multisets of literals.

LK restricted to clauses has only four inference rules:

• identity
• cut (propositional resolution)
• contraction (propositional factoring)
• weakening

It is obvious that these four rules are complete for deducing clauses, i.e.,

Proposition 1 For any clause $C$ and set of clauses ${\cal S}$, we have ${\cal S} \models C$ if and only if ${\cal S} \vdash C$.

Refutation proof converts the problem of ${\cal S} \vdash C$ to ${\cal S} \cup N(C) \vdash \bot$, where $N(C) = \{\{\bar{A}\} \mid A \in C\}$ is the collection of clauses representing the negation of $C$.

It is clear that ${\cal S} \vdash C$ if and only if ${\cal S} \cup N(C) \vdash \bot$. Our four-rule system is still adequate for proving the converted problem, but we notice that we don't need identity and weakening any more. The remaining two rules are called the "resolution proof procedure".

Proposition 2 For any clause $C$ and set of clauses ${\cal S}$, we have ${\cal S} \models C$ if and only if ${\cal S} \cup N(C) \vdash \bot$ using only cut and contraction.

The point of converting the problem to refutation proofs is two-fold:

• We have a better opportunity to guide the proof search by letting $N(C)$ drive it.
• We have a handle on full predicate logic, whose formulas can be transformed to CNF upto satisfiability.

Is the "right" proof theoretic view of resolution just that it is a fragment of the sequent calculus that suffices for checking satisfiability of formulae in CNF?

Indeed!

Answer 2

1)

The only non-structural rule is resolution (on atoms).

$$ \varphi\lor C, \psi\lor \overline{C} \over \varphi\lor \psi$$

However a rule by itself doesn't give a proof system. See part 3.

2)

Think about it this way: is Gentzen's sequent calculus PK complete if we are using some other set of connectives in place of $\{\land, \lor, \lnot\}$? The logical connectives one uses is important for logic results like completeness. It is with respect to the formulas in that language that a proof system can be complete. PK cannot talk about formulas in some other language. Your issue with resolution is similar. Yes, if we are talking about completeness regarding general formulas with $\{\land, \lor, \lnot\}$ connectives then resolution is not complete, but neither are sequent calculus and natural deduction with respect to formulas that are not in their language.

As long as there is a "nice" translation from one language to another one we can talk about completeness. What matters essentially is that we can translate formulas from one to the other one and vice versa efficiently. You can check Robert Reckhow's thesis where he deals with the issue of connective and shows that for Frege systems the length of proofs doesn't change more than a polynomial so it is fine in a sense to pick any set of adequate connectives that you like.

The situation for resolution is similar. By reduction from SAT to 3SAT we can restrict our attention to CNFs and the transformation can be done very efficiently.

Note that resolution is not alone here, the issue applies to other proof systems also. Take for example Bounded-Depth Frege where the depth of formulas must to be bounded by a constant so by definition it cannot prove any unbounded-depth families of formulas.

3)

Let us define what it means for a proposition proof system to be complete. By Cook-Reckhow, a propositional proof system $P$ is a binary relation $\vdash_P$ satisfying the following conditions:

• Efficiency: $\vdash_P$ is polynomial-time decidable, i.e. given a string $\varphi$ (formula) and a string $\pi$ (proof), we can decide if $\pi$ is a $P$-proof of a $\varphi$ in polynomial-time.

• Soundness: if there is a $P$-proof for $\varphi$, then $\varphi$ is true.

• Completeness: if $\varphi$ is true, then there is a $P$-proof for $\varphi$.

The definition is very general and doesn't talk about the structure of the proof at all. Anything that satisfies these conditions is a propositional proof system.

Which class of formula should we consider in these items? Different classes of formulas have been considered and the first treatment of the issue I know of is Robert Reckhow's thesis where he shows that as long as one is concerned with Frege systems it doesn't matter which adequate set of connectives one uses, all of them are equivalent.

Regarding resolution, if one really wants to have completeness regarding all formulas and not just CNFs one can incorporate a fixed polynomial-time translation from arbitrary formulas to CNFs into the proof system with no problem as the translation is polynomial-time computable.

In any case, the resolution proof system works as follows: it checks if the $\pi$ is a derivation of $\bot$ using resolution rule from the set of clauses obtained from translation of $\lnot \varphi$ to clauses. This is the propositional proof system people refer to as resolution propositional proof system.

4)

Resolution is fine as it is, however one can also think of it in the way you mentioned, i.e. we can of course think of it as the cut rule when cut formula is a positive atoms by moving the negative atoms to the antecedent and keeping the positive ones in the succedent:

$$ \Rightarrow \varphi, C \hspace{1cm} C \Rightarrow \psi \over \Rightarrow \varphi, \psi$$

Note that what defines the power of a propositional proof system in subsystems of Frege (and even in subsystems of more powerful similar propositional proof systems like quantified propositional logic $G$) is mainly the class of formulas that one can cut. I think we can take Gentzen's PK and just restrict the cut rule to apply to such cut formulas and the resulting proof system will be not more powerful than resolution in proving CNFs. Any proof of a CNFs (written in the sequent form with positive atoms) can only have similar sequents, i.e. more complicated formulas are of no use in proving CNFs (note that the cut is the only rule that can remove formulas from sequents).

ps: My answer is mainly from proof complexity theoretic perspective. You may want to check other perspectives like structural proof theory.

References:

• Robert A. Reckhow, "On the Lengths of Proofs in the Propositional Calculus", 1976.