×

Automation of reasoning. 2: Classical papers on computational logic 1967- 1970. (English) Zbl 0567.03002

Symbolic Computation. Artificial Intelligence. Berlin etc.: Springer- Verlag. XII, 637 p. DM 108.00 (1983).
The second volume of the Classical Papers on Computational Logic contains the fundamental works during 1967-1970. The volume begins with an original review paper of L. Wos and L. Henschen: ”Automated theorem proving 1965-1970 (pp. 1-24). It represents an authorized critical history of the most important achievements in the field, a guide containing concise and objective evaluations of the ideas, prefiguring the valuable future directions. Summarizing this paper we can give an impression of the whole volume.
The strong impact of the J. A. Robinson’s resolution strategy was reflected by a great number of the papers concerning resolution with some aspects. Since the straightforward application of resolution generates too many clauses, three important problems naturally arose: developing strategies for inference rules, more powerful inference rules and more effective ways of representing problems. As inference rules are discussed Pl-resolution and hyper-resolution, introduced by J. A. Robinson, and paramodulation, introduced by L. Wos and G. Robinson. Four classes of automated theorem-proving strategies are identified: Guiding strategies (unit preference, introduced by L. Wos, G. Robinson, D. Carson; selection strategies, used by R. Kowalsky and J. Slagle; R. Overbeek’s weighting), Restriction strategies (set-of-support strategy, introduced by L. Wos, G. Robinson, D. Carson; unit restriction, by the same authors; linear resolution of D. Loveland and D. Luckham), Simplification strategies (demodulation of L. Wos, G. Robinson, D. Carson, L. Shalla) and Pruning strategies (subsumption, proposed by J. A. Robinson). Another interesting topic discussed in many papers in the period was the poblem of completeness (and other logical properties) for the strategies developed, since this property assures, theoretically, at least one proof for each theorem. Concerning testing, implementation and experiments with the theorem proving programs, the quite important idea is that the various computer programs contributed very much more than a means of idea testing; through their use important additions to the theory were found. Along with the ”logical” (logic based) approach to the automation of reasoning was the ”human” approach, attempting to study and simulate human reasoning. Around 1970 this trend received more and more attention, the most important areas being question-answering (C. Green’s contributions) and the application of theorem proving to program verification. The features of the seventies are discussed and their conclusions are outlined. As the authors remark, the automated deduction already proved its maturity by realizing incontestable achievements and entered now in a new phase, that of spreading its force and influence in a large number of scientific, technological and industrial areas.
As we already observed for the first volume of the series, the extraordinary work and competence of those who did the selection and the intrinsic value of each paper make any further commentaries useless.
The second volume contains the following papers: R. W. Binkley and R. L. Clark: ”A cancellation algorithm for elementary logic” (pp. 27-47) [Theoria 33, 79-97 (1967)];
S. Yu. Maslov: ”An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus” (pp. 48-54) [Dokl. Akad. Nauk SSSR 172, 22-25 (1967); English translation in Soviet Math., Dokl. 8, 16-19 (1967; Zbl 0165.318)];
J. R. Slagle: ”Automatic theorem proving with renamable and semantic resolution” (pp. 55-65) [J. Assoc. Comput. Mach. 14, 687-697 (1967; Zbl 0157.024)];
L. T. Wos, G. A. Robinson, D. F. Carson and L. Shalla: ”The concept of demodulation in theorem proving” (pp. 66-84) [ibid. 14, 698-709 (1967; Zbl 0157.024)];
P. B. Andrews: ”Resolution with merging” (pp. 85-101) [ibid. 15, 367-381 (1968; Zbl 0182.025)];
P. B. Andrews: ”On simplifying the matrix of a wff” (pp. 102-116) [J. Symb. Logic 33, 180-192 (1968; Zbl 0157.335)];
D. W. Loveland: ”Mechanical theorem-proving by model elimination” (pp. 117-134) [J. Assoc. Comput. Mach. 15, 236-251 (1968; Zbl 0162.028)];
J. A. Robinson: ”The generalized resolution principle” (pp. 135- 151) [Machine Intelligence 3, 77-93 (1968; Zbl 0195.311)];
J. A. Robinson: ”New directions in mechanical theorem proving” (pp. 152-158) [Inf. Processing, Proc. IFIP Congr., Edinburgh 1968, 1, 63-69 (1969; Zbl 0213.024)];
N. G. de Bruijn: ”AUTOMATH, a language for mathematics” (pp. 159-200) [TH Report 68-WSK-05, Techn. Univ. Eindhoven (1968)];
J. R. Guard, F. C. Oglesby, J. H. Bennett and L. G. Settle: ”Semi-automated mathematics” (pp. 203-216) [J. Assoc. Comput. Mach. 16, 49-62 (1969; Zbl 0175.282)];
R. Kowalski and P. J. Hayes: ”Semantic trees in automatic theorem-proving” (pp. 217-232) [Machine Intelligence 4, 87-101 (1969; Zbl 0217.540)];
D. W. Loveland: ”A simplified format for the model elimination theorem-proving procedure” (pp. 233-248) [J. Assoc. Comput. Mach. 16, 349-363 (1969; Zbl 0183.296)];
D. W. Loveland: ”Theorem-provers combining model elimination and resolution” (pp. 249-263) [Machine Intelligence 4, 73-86 (1969; Zbl 0257.68083)];
S. Yu. Maslov: ”Relationship between tactics of the inverse method and the resolution method” (pp. 264-272) [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 16, 137-146 (Russian) (1969; Zbl 0199.315)];
J. B. Morris: ”E-resolution: extension of resolution to include the equality relation” (pp. 273-282) [Proc. Int. Joint. Conf. Artif. Intell., Washington D. C., 287-294 (1969)];
D. Prawitz: ”Advances and problems in mechanical proof procedures” (pp. 283-297) [Machine Intelligence 4, 59-71 (1969; Zbl 0257.68082)];
G. Robinson and L. Wos: ”Paramodulation and theorem-proving in first-order theories with equality” (pp. 298-313) [ibid. 4, 135-150 (1969; Zbl 0219.68047)];
R. Anderson: ”Completeness results for E-resolution” (pp. 317-320) [AFIPS 1970 Spring Joint Comput. Conf., 652-656 (1970)];
R. Anderson and W. W. Bledsoe: ”A linear format for resolution with merging and a new technique for establishing completeness” (pp. 321-330) [J. Assoc. Comput. Mach. 17, 525-534 (1970; Zbl 0199.315)];
C. L. Chang: ”The unit proof and the input proof in theorem proving” (pp. 331-341) [ibid. 17, 698-707 (1970; Zbl 0212.342)];
D. E. Knuth and P. B. Bendix: ”Simple word problems in universal algebras” (pp. 342-376) [Comput. Probl. Abstr. Algebra, Proc. Conf. Oxford 1967, 263-297 (1970; Zbl 0188.049)];
R. Kowalski: ”The case for using equality axioms in automatic demonstration” (pp. 377-398) [Lect. Notes Math. 125, 112-127 (1970; Zbl 0226.68045)];
D. W. Loveland: ”A linear format for resolution” (pp. 399-416) [ibid. 125, 147-162 (1970; Zbl 0202.015)];
J. Allen and D. Luckham: ”An interactive theorem-proving program” (pp. 417-434) [Machine Intelligence 5, 321-326 (1970)];
D. Luckham: ”Refinement theorems in resolution theory” (pp. 435-465) [Lect. Notes Math. 125, 163- 190 (1970; Zbl 0216.241)];
G. S. Tsejtin: ”On the complexity of derivation in propositional calculus” (pp. 466-483) [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 8, 234-259 (Russian) (1968; Zbl 0197.001)];
P. B. Andrews: ”Resolution in type theory” (pp. 487-507) [J. Symb. Logic. 36, 414-432 (1971; Zbl 0231.02038)];
W. W. Bledsoe: ”Splitting and reduction heuristics in automatic theorem proving” (pp. 508-530) [Artif. Intell. 2, 55-77 (1971; Zbl 0221.68052)];
G. V. Davydov, S. Yu. Maslov, G. E. Mints, V. P. Orevkov and A. O. Slisenko: ”A computer algorithm for the determination of deducibility on the basis of the inverse method” (pp. 531-541) [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 16, 8-19 (Russian) (1969; Zbl 0198.036)];
R. Kowalski and D. Kuehner: ”Linear resolution with selection function” (pp. 542-577) [Artif. Intell. 2, 227- 260 (1971; Zbl 0234.68037)];
L. T. Wos and G. A. Robinson: ”Maximal models and refutation completeness: Semidecision procedures in automatic theorem proving” (pp. 578-608) [Word Probl., Decision Probl. Burnside Probl. Group Theory, Stud. Logic. Found. Math. 71, 609-639 (1973; Zbl 0283.68058)]; Bibliography on computational logic (pp. 609- 637).
Reviewer: N.Curteanu

MSC:

03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
01A75 Collected or selected works; reprintings or translations of classics