Table of contents: The eighth conference has been reviewed (see Zbl 0598.00015).
The fifty-two papers and twenty-one abstracts in this collection include the following:
Hantao Zhang and Deepak Kapur, First-order theorem proving using conditional rewrite rules (pp. 1–20); Tie Cheng Wang, Elements of \(Z\)-module reasoning (pp. 21–40); M. R. Donat and L. A. Wallen, Learning and applying generalised solutions using higher order resolution (pp. 41–60); Amy Felty and Dale Miller, Specifying theorem provers in a higher-order logic programming language (pp. 61–80); V. S. Subrahmanian, Query processing in quantitative logic programming (pp. 81–100);
David A. Basin, An environment for automated reasoning about partial functions (pp. 101–110); Alan Bundy, The use of explicit plans to guide inductive proofs (pp. 111–120); Donald Simon, Checking natural language proofs (pp. 141–150); Marc Bezem, Consistency of rule-based expert systems (pp. 151–161); Hantao Zhang, Deepak Kapur and Mukkai S. Krishnamoorthy, A mechanizable induction principle for equational specifications (pp. 162–181); Jean Gallier, Paliath Narendran, David Plaisted, Stan Raatz and Wayne Snyder, Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time (pp. 182–196); Michael A. McRobbie, Robert K. Meyer and Paul B. Thistlewaite, Towards efficient ”knowledge-based” automated theorem proving for nonstandard logics (pp. 197–217);
A. A. Aaby and K. T. Narayana, Propositional temporal interval logic is PSPACE complete (pp. 218–237); Jack Minker and Arcot Rajasekar, Procedural interpretation of non-Horn logic programs (pp. 278–293); Shan Chi and Lawrence J. Henschen, Recursive query answering with non-Horn clauses (pp. 294–312); T. Wakayama and T. H. Payne, Case inference in resolution-based languages (pp. 313–322); Louise E. Moser, A decision procedure for unquantified formulas of graph theory (pp. 344–357); Wolfram Büttner, Unification in finite algebras is unitary(?) (pp.368–377); Manfred Schmidt-Schauß Unification in a combination of arbitrary disjoint equational theories (pp. 378–396); Karl-Hans Bläsius and Jörg H. Siekmann, Partial unification for graph based equational reasoning (pp. 397–414).
Bishop Brock, Shaun Cooper and William Pierce, Analogical reasoning and proof discovery (pp. 454–468); Larry Hines, Hyper-chaining and knowledge-based theorem proving (pp. 469–486); Luis Fari nas del Cerro and Andreas Herzig, Linear modal deductions (pp. 487–499);
Hans Jürgen Ohlbach, A resolution calculus for modal logics (pp. 500–516); Hans-Jürgen Bürckert, Solving disequations in equational theories (pp. 517–526); Emmanuel Kounalis and Michael Rusinowitch, On word problems in Horn theories (pp. 527–537); Nachum Dershowitz, Mitsuhiro Okada and G. Sivakumar, Canonical conditional rewrite systems (pp. 538–549); Paul Jacquet, Program synthesis by completion with dependent subtypes (pp. 550–562); Thomas Käufl, Reasoning about systems of linear inequalities (pp. 563–572); Rolf Socher, A subsumption algorithm based on characteristic matrices (pp. 573–581); Arkady Rabinov, A restriction of factoring in binary resolution (pp.582–591); Philippe Besnard and Pierre Siegel, Supposition-based logic for automated nonmonotonic reasoning (pp. 592–601);
Christoph Walther, Argument-bounded algorithms as a basis for automated termination proofs (pp. 602–621); Leo Marcus and Timothy Redmond, Two automated methods in implementation proofs (pp. 622–642); Mark Franzen and Lawrence J. Henschen, A new approach to universal unification and its application to AC-unification (pp. 643–657); Neil V. Murray and Erik Rosenthal, An implementation of a dissolution-based system employing theory links (pp. 658–674); Ilkka Niemelä, Decision procedure for autoepistemic logic (pp. 675–684); Peter K. Malkin and Errol P. Martin, Logical matrix generation and testing (pp. 685–693); Rakesh M. Verma and I. V. Ramakrishnan, Optimal time bounds for parallel term matching (pp. 694–703);
William McCune, Challenge equality problems in lattice theory (pp. 704–709); Frank Pfenning, Single axioms in the implicational propositional calculus (pp. 710–713); Larry Wos and William McCune, Challenge problems focusing on equality and combinatory logic: evaluating automated theorem-proving programs (pp. 714–729); Rick L. Stevens, Challenge problems from nonassociative rings for theorems provers (pp. 730–734).
The articles of this volume will be reviewed individually under the abbreviation “Automated deduction, Proc. 9th Int. Conf., Argonne/Ill. 1988, Lect. Notes Comput Sci. 310”.