<h3>1)</h3>
<p>The only non-structural rule is resolution (on atoms).</p>
<p><span class="math-container">$$ \varphi\lor C, \psi\lor \overline{C} \over \varphi\lor \psi$$</span></p>
<p>However a rule by itself doesn't give a proof system. See part 3.</p>
<h3>2)</h3>
<p>Think about it this way: is Gentzen's sequent calculus PK complete if we are using some other set of connectives in place of <span class="math-container">$\{\land, \lor, \lnot\}$</span>? 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 <span class="math-container">$\{\land, \lor, \lnot\}$</span> connectives then resolution is not complete, but neither are sequent calculus and natural deduction with respect to formulas that are not in their language.</p>
<p>As long as there is a &quot;nice&quot; 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 <a href="http://www.cs.toronto.edu/%7Esacook/homepage/reckhow_thesis.pdf" rel="noreferrer">Robert Reckhow's thesis</a> 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 <em>adequate</em> connectives that you like.</p>
<p>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.</p>
<p>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.</p>
<h3>3)</h3>
<p>Let us define what it means for a proposition proof system to be complete. By Cook-Reckhow, a propositional proof system <span class="math-container">$P$</span> is a binary relation <span class="math-container">$\vdash_P$</span> satisfying the following conditions:</p>
<ul>
<li><p>Efficiency: <span class="math-container">$\vdash_P$</span> is polynomial-time decidable, i.e. given a string <span class="math-container">$\varphi$</span> (formula) and a string <span class="math-container">$\pi$</span> (proof), we can decide if <span class="math-container">$\pi$</span> is a <span class="math-container">$P$</span>-proof of a <span class="math-container">$\varphi$</span> in polynomial-time.</p>
</li>
<li><p>Soundness: if there is a <span class="math-container">$P$</span>-proof for <span class="math-container">$\varphi$</span>, then <span class="math-container">$\varphi$</span> is true.</p>
</li>
<li><p>Completeness: if <span class="math-container">$\varphi$</span> is true, then there is a <span class="math-container">$P$</span>-proof for <span class="math-container">$\varphi$</span>.</p>
</li>
</ul>
<p>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.</p>
<p>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 <a href="http://www.cs.toronto.edu/%7Esacook/homepage/reckhow_thesis.pdf" rel="noreferrer">Robert Reckhow's thesis</a> 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.</p>
<p>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.</p>
<p>In any case, the resolution proof system works as follows: it checks if the <span class="math-container">$\pi$</span> is a derivation of <span class="math-container">$\bot$</span> using resolution rule from the set of clauses obtained from translation of <span class="math-container">$\lnot \varphi$</span> to clauses. This is the propositional proof system people refer to as resolution propositional proof system.</p>
<h3>4)</h3>
<p>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:</p>
<p><span class="math-container">$$ \Rightarrow \varphi, C \hspace{1cm} C \Rightarrow \psi \over \Rightarrow \varphi, \psi$$</span></p>
<p>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 <span class="math-container">$G$</span>) 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).</p>
<p>ps:
My answer is mainly from proof complexity theoretic perspective. You may want to check other perspectives like <em>structural proof theory</em>.</p>
<p>References:</p>
<ul>
<li>Robert A. Reckhow, &quot;<a href="http://www.cs.toronto.edu/%7Esacook/homepage/reckhow_thesis.pdf" rel="noreferrer">On the Lengths of Proofs in the Propositional Calculus</a>&quot;, 1976.</li>
</ul>

CC BY-SA 3.0
2013-02-23T22:33:00.357Z
Thanks for your answer. I see how Uday is saying similar things, but I found I could follow his answer more easily.
Vijay D
CC BY-SA 3.0
2013-02-24T04:51:14.133Z
@VijayD, sure, no problem. :)
Kaveh
CC BY-SA 3.0
2013-02-21T02:48:33.253Z
2013-02-22T22:57:51.693Z
2020-06-17T09:38:08.363Z
Kaveh
<p><i>What proof system is being considered when discussing resolution? Is it just the resolution rule? What are the other rules?</i></p>

<p>I discuss resolution in the context of "clauses", which are sequents made up of only <em>literals</em>.  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 <em>multisets</em> of literals.  </p>

<p>LK restricted to clauses has only four inference rules:</p>

<ul>
<li>identity</li>
<li>cut (propositional resolution)</li>
<li>contraction (propositional factoring)</li>
<li>weakening</li>
</ul>

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

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

<p>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$.</p>

<p>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".</p>

<p><strong>Proposition 2</strong> 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.</p>

<p>The point of converting the problem to refutation proofs is two-fold:</p>

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

<p><i>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?</i></p>

<p>Indeed!</p>

CC BY-SA 3.0
2013-02-22T21:24:42.727Z
Thanks Uday. One question: The cut rule still keep the clauses from the original formula round in the consequent. In resolution, these are "optimized" away with only one clause in the consequent. Would you agree that that resolution is a minimal or local rule because of all clauses not appearing in the rule?
Vijay D
CC BY-SA 3.0
2013-02-22T22:17:12.707Z
@VijayD.  We are using precisely the cut rule, but in a different way from Gentzen.  Gentzen proofs would be of the form ${} \vdash C$, where there are no "axioms", whereas in resolution we are producing proofs with axioms ${\cal S} \vdash C$.  You might like to look at this paper [Clausal Completion](http://www.cs.bham.ac.uk/~udr/papers/clausal.ps).
Uday Reddy
CC BY-SA 3.0
2013-02-23T00:16:55.080Z
could you also add to your answer what you think is an one-sentence, accurate description of the completeness of resolution?
Vijay D
CC BY-SA 3.0
2013-02-23T21:53:27.587Z
@VijayD. There were two "if and only if" statements in my original answer, which were the two completeness properties.  For clarity, I have highligted them as Propositions for you. (I am not yet sure where your confusion lies.  Perhaps it has to do with which language we are working with, as Kaveh has implied?)
Uday Reddy
CC BY-SA 3.0
2013-02-23T22:31:38.077Z
The highlights you have added helped. I realise that my confusion is not technical but about terminology. It appeared that one could say resolution was complete, or that it was incomplete and be correct in both respects. Your answers convince me I should say resolution is complete and emphasise the different setting, compared to the sequent calculus. Resolution is incomplete if I take it out of its intended context which is misrepresenting resolution. Do all agree?
Vijay D
CC BY-SA 3.0
2013-02-24T08:44:16.440Z
@VijayD. I don't think you can say that resolution is "incomplete".  All you have said in your original question was that the transformations necessary to put propositional formulas into clausal form are "unsatisfying" to you.  That does not mean that they are "incomplete".
Uday Reddy
CC BY-SA 3.0
2013-02-22T20:16:58.067Z
2013-02-23T22:00:49.210Z
2013-02-23T22:00:49.210Z
Uday Reddy
<p>This question is about propositional logic and all occurrences of "resolution" should be read as "propositional resolution".</p>

<p>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. </p>

<p><strong>Soundness and Completeness</strong></p>

<p>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. </p>

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

<p><strong>The Resolution Rule</strong></p>

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

<p>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.</p>

<p>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. </p>

<p><strong>Incompleteness of resolution</strong></p>

<p>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 <em>refutation complete</em> meaning if we have $\models F \implies \bot$ then we can derive $\bot$ from $F$ using resolution.</p>

<p>Consider the formule</p>

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

<p>In Gentzen's system LK or using natural deduction, I can <em>derive</em> 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. </p>

<p>I see how I can prove the validity of this implication using resolution:</p>

<ol>
<li>Consider the formula $\neg (\varphi \implies \psi)$</li>
<li>Turn the formula above into CNF either using standard distributivity rules or using the Tseitin transformation</li>
<li>Derive $\bot$ from the transformed formula using resolution.</li>
</ol>

<p>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.</p>

<p><strong>Questions</strong></p>

<p>Given all that above, my questions are:</p>

<ol>
<li>What proof system is being considered when discussing resolution? Is it just the resolution rule? What are the other rules?</li>
<li>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?</li>
<li>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?</li>
<li>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?</li>
</ol>

CC BY-SA 3.0
2013-02-21T00:23:48.547Z
(1) CNF formulas with just resolution (or, if you do QBF, then QCNF formulas with resolution & forall-reduction); (2) Yes, it's refutation complete, and still a slightly different meaning, namely if $\psi\models\bot$ then $\psi\vdash\bot$.
Radu GRIGore
CC BY-SA 3.0
2013-02-21T00:41:12.987Z
roughly similar question here. thx for posting. basically, iiuc/afaik, [resolution](http://en.wikipedia.org/wiki/Resolution_%28logic%29) is used for systems much more than 1st order logic, but within 1st order logic it is "sound/complete", although that is not always very well described, because it is often just used for refutation proofs. in the "larger" systems, where terms are not merely boolean variables but eg existential qualifiers etc, it is not complete. the field of logic does not standardize its definitions of terminology too well, theres a lot of "overloading" of terms etc....
vzn
CC BY-SA 3.0
2013-08-13T13:43:03.240Z
That's why some people say it is "*refutationally* complete", e.g. L. Bachmair and H. Ganzinger, “Resolution theorem proving,” Handbook of automated reasoning, vol. 1, pp. 19–99, 2001.
Trylks
CC BY-SA 3.0
2013-08-13T19:33:34.967Z
The question discusses refutational completeness.
Vijay D
<lo.logic><terminology><proof-complexity><proof-theory><resolution>
Is propositional resolution a complete proof system?
Vijay D
# Is propositional resolution a complete proof system?

(Asked by: username_0 on 2013-02-20)

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?

**Tags:** lo.logic, terminology, proof-complexity, proof-theory, resolution

> **Comments:**
> **username_1**: (1) CNF formulas with just resolution (or, if you do QBF, then QCNF formulas with resolution & forall-reduction); (2) Yes, it's refutation complete, and still a slightly different meaning, namely if $\psi\models\bot$ then $\psi\vdash\bot$.  
> **username_2**: roughly similar question here. thx for posting. basically, iiuc/afaik, [resolution](http://en.wikipedia.org/wiki/Resolution_%28logic%29) is used for systems much more than 1st order logic, but within 1st order logic it is "sound/complete", although that is not always very well described, because it is often just used for refutation proofs. in the "larger" systems, where terms are not merely boolean variables but eg existential qualifiers etc, it is not complete. the field of logic does not standardize its definitions of terminology too well, theres a lot of "overloading" of terms etc....  
> **username_3**: That's why some people say it is "*refutationally* complete", e.g. L. Bachmair and H. Ganzinger, “Resolution theorem proving,” Handbook of automated reasoning, vol. 1, pp. 19–99, 2001.  
> **username_0**: The question discusses refutational completeness.  

---

## 2 answers

### Answer by username_5 on 2013-02-22. Score: 10 | Accepted answer

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

> **Comments:**
> **username_0**: Thanks Uday. One question: The cut rule still keep the clauses from the original formula round in the consequent. In resolution, these are "optimized" away with only one clause in the consequent. Would you agree that that resolution is a minimal or local rule because of all clauses not appearing in the rule?  
> **username_5**: @VijayD.  We are using precisely the cut rule, but in a different way from Gentzen.  Gentzen proofs would be of the form ${} \vdash C$, where there are no "axioms", whereas in resolution we are producing proofs with axioms ${\cal S} \vdash C$.  You might like to look at this paper [Clausal Completion](http://www.cs.bham.ac.uk/~udr/papers/clausal.ps).  
> **username_0**: could you also add to your answer what you think is an one-sentence, accurate description of the completeness of resolution?  
> **username_5**: @VijayD. There were two "if and only if" statements in my original answer, which were the two completeness properties.  For clarity, I have highligted them as Propositions for you. (I am not yet sure where your confusion lies.  Perhaps it has to do with which language we are working with, as username_4 has implied?)  
> **username_0**: The highlights you have added helped. I realise that my confusion is not technical but about terminology. It appeared that one could say resolution was complete, or that it was incomplete and be correct in both respects. Your answers convince me I should say resolution is complete and emphasise the different setting, compared to the sequent calculus. Resolution is incomplete if I take it out of its intended context which is misrepresenting resolution. Do all agree?  
> **username_5**: @VijayD. I don't think you can say that resolution is "incomplete".  All you have said in your original question was that the transformations necessary to put propositional formulas into clausal form are "unsatisfying" to you.  That does not mean that they are "incomplete".  

---

### Answer by username_4 on 2013-02-21. Score: 13

### 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](http://www.cs.toronto.edu/%7Esacook/homepage/reckhow_thesis.pdf) 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](http://www.cs.toronto.edu/%7Esacook/homepage/reckhow_thesis.pdf) 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](http://www.cs.toronto.edu/%7Esacook/homepage/reckhow_thesis.pdf)", 1976.

> **Comments:**
> **username_0**: Thanks for your answer. I see how Uday is saying similar things, but I found I could follow his answer more easily.  
> **username_4**: @VijayD, sure, no problem. :)  

---

