This series of volumes, the first covering 1957 and 1966 and the second 1967 to 1970, contains those papers which have shaped and influenced the field of computational logic and makes available the classical work, which in many cases is difficult to obtain or had not previously appeared in English. The main purpose of this series is to evaluate the ideas of the time and to select those papers, which can now be regarded as classics after more than a decade of intensive research.

The connection graph proof procedure (or clause graph resolution as it is more commonly called today) is a theorem proving technique due to Robert Kowalski. It is a negative test calculus (a refutation procedure) based on resolution.Due to an intricate deletion mechanism that generalises the well-known purity principle, it substantially refines the usual notions of resolution-based systems and leads to a largely reduced search space. The dynamic nature of the clause graph upon which this refutation procedure is based, poses novel meta-logical problems previously unencountered in logical deduction systems. Ever since its invention in 1975 the soundness, confluence and (strong) completeness of the procedure have been in doubt in spite of many partial results.Th is paper provides an introduction to the problem as well as an overview of the main results that have been obtained in the last twenty-five years.

Categories and Subject Descriptors: F.1.3 [Computation by Abstract Devices]: Complexity Classes-machine independent complexity: F.2.2 [Analysis of Algorithms and Problem Complexity): Nonnumerical Algorithms and Problems-complexity of proof procedures; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic-mechanical theorem proving, proof theory, I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving-deduction, resolution.

but essential properties. For example, such a property is the ability, in theory, to find at least one proof for each theorem. It was deemed important to know which types of reasoning lacked this property. In response to these two pressures, a very evident trend in research occurred.

For automated theorem proving it is shown in [1] how formulas containing equivalence connectives can be treated so as to avoid excessive storage space explosion during runtime. The approach is logically based and is not an implementation technique. In [1] the approach is first restricted to the class of propositional formulas in which, apart from negation, only the equivalence and non-equivalence connectives appaer. For example take ((A ⇔ B) ⇎ C) ⇔ (D ⇎ E), where A,B,C,D,E are literals. Although computing time is not reduced the storage space required to prove this formula not valid is no more than the formula itself. First, in one pass, the literals are found and the proof can be carried out simply by placing negation connectives in front of the literals (i.e. the literals are ‘weighted’ with negations depending upon the number of ⇔’s and ⇎’s). Then the weighted literals are treated as a conjunction. If this conjunction does not contain a contradiction then the procedure stops. Otherwise the weighting and testing of the resulting conjunction for a contradiction is done 2n-1 times, where n is the number of literals.If conjuncions are found each time then the negation of the given formula is valid. The main theorem in [1], based on combinatorial considerations, shows how the literals are to be weighted according to a simple formula. For formulas of the above class no recursion or splitting is needed and it can easily be shown that the space complexity is reduced from 0(2n-1) to 0(n).

The connection graph proof procedure of R. Kowalski is extended to the case of equality. The extension is achieved through the introduction of special links connecting those terms that can be paramodulated upon. Completeness and consistency of the resulting proof procedure are shown.