zbMATH — the first resource for mathematics

Examples
Geometry Search for the term Geometry in any field. Queries are case-independent.
Funct* Wildcard queries are specified by * (e.g. functions, functorial, etc.). Otherwise the search is exact.
"Topological group" Phrases (multi-words) should be set in "straight quotation marks".
au: Bourbaki & ti: Algebra Search for author and title. The and-operator & is default and can be omitted.
Chebyshev | Tschebyscheff The or-operator | allows to search for Chebyshev or Tschebyscheff.
"Quasi* map*" py: 1989 The resulting documents have publication year 1989.
so: Eur* J* Mat* Soc* cc: 14 Search for publications in a particular source with a Mathematics Subject Classification code (cc) in 14.
"Partial diff* eq*" ! elliptic The not-operator ! eliminates all results containing the word elliptic.
dt: b & au: Hilbert The document type is set to books; alternatively: j for journal articles, a for book articles.
py: 2000-2015 cc: (94A | 11T) Number ranges are accepted. Terms can be grouped within (parentheses).
la: chinese Find documents in a given language. ISO 639-1 language codes can also be used.

Operators
a & b logic and
a | b logic or
!ab logic not
abc* right wildcard
"ab c" phrase
(ab c) parentheses
Fields
any anywhere an internal document identifier
au author, editor ai internal author identifier
ti title la language
so source ab review, abstract
py publication year rv reviewer
cc MSC code ut uncontrolled term
dt document type (j: journal article; b: book; a: book article)
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-06Proceedings of conferences (mathematical logic)
68-06Proceedings of conferences (computer science)
03B35Mechanical theorem proving; logical operations
68T15Theorem proving (deduction, resolution, etc.)
01A75Collected or selected works