What paper proved the completeness of Ordered Resolution?

Question

I am having trouble finding online the original proof of the completeness of Ordered Resolution. Does anyone happen to know where it exists? Thanks!

Answer 1

I have found at least a partial answer to this question. In "Resolution Methods for the Decision Problem" (1993 - C. Fermüller, A. Leitsch, T. Tammet, N. Zamov), the authors write :

“As shown by S. Maslov (see [Mas68], [Mas71]), the acyclicity of ‘>’ (therefore also conditions (A) and (B)) is enough for the resolution with a ‘>’-refinement to be complete for ground formulas.”

In other words, the Completeness of Ordered Resolution (for the case where the ordering on literals is acylical, and where none of the literals contain variables) is proven, in the papers cited as [Mas68] and [Mas71].

The citations correspond to :

• [Mas68]: S.Y. Maslov : The Inverse Method for Establishing Deducibility for Logical Calculi. Trudy Mat. Inst. Steklov 98 (1968) 26-87= Proc. Steklov. Inst. Math. 98 (1968) 25-96, MR 40 =5416; 43 =4620.

• [Mas71]: S.Y. Maslov : Proof-Search Strategies for Methods of the Resolution Type. Machine Intelligence 6 (American Elsevier), 1971, pp. 77-90.

Luckily I was able to get help from users on the Logic sub-reddit in tracking down the papers (see this comment).

The comment provided me with the following information :

The first paper is available online, but only in Russian (here).

Both papers, however, are available in the collections of physical libraries. The location of the nearest physical library containing the papers can be found below :

• for first paper

• for second paper

Answer 2

The Chapter "Resolution Theorem Proving" of the Handbook of Automated Reasoning contains a short history of ordered resolution in Section 11:

https://lawrencecpaulson.github.io/papers/bachmair-hbar-resolution.pdf

Slagle was the first to introduce the idea of ordering atoms, attributing it to Reynolds:

https://dl.acm.org/doi/pdf/10.1145/321420.321428

However, this variant of resolution did not have a redundancy criterion. So I would say that the original proof of the completeness of ordered resolution is identical with the one for paramodulation:

Bachmair L. and Ganzinger H.: On restrictions of ordered paramodulation with simplification, 1990. https://link.springer.com/chapter/10.1007/3-540-52885-7_105