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:
- Consider the formula $\neg (\varphi \implies \psi)$
- Turn the formula above into CNF either using standard distributivity rules or using the Tseitin transformation
- 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.
Given all that above, my questions are:
- What proof system is being considered when discussing resolution? Is it just the resolution rule? What are the other rules?
- 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?
- 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?
- 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?