Table of contents: The sixth conference has been reviewed (see Zbl 0476.00025).
Contents: Jorg H. Siekmann, Universal unification (pp. 1–42); Ewing L. Lusk and Ross A. Overbeek, A portable environment for research in automated reasoning (pp. 43–52); Deepak Kapur and Balakrishnan Krishnamurthy, A natural proof system based on rewriting techniques (pp. 53–64); Jussi Ketonen, EKL—a mathematically oriented proof checker (pp. 65–79); Silvio Ursic, A linear characterization of NP-complete problems (pp. 80–100);
Allen Van Gelder, A satisfiability tester for nonclausal propositional calculus (pp. 101–112); Ana R. Cavalli and Luis Farinas del Cerro, A decision method for linear temporal logic (pp. 113–127); D. Lankford, G. Butler and A. Ballantyne, A progress report on new decision algorithms for finitely presented abelian groups (pp. 128–141); Philippe Le Chenadec, Canonical forms in finitely presented algebras (pp. 142–165); Pierre Lescanne, Term rewriting systems and algebra (pp. 166–174); Jean-Pierre Jouannaud and Miguel Munoz, Termination of a set of rules modulo a set of equations (pp. 175–193); François Fages, Associative-commutative unification (pp. 194–208);
Donald Simon, A linear time algorithm for a subcase of second order instantiation (pp. 209–223); Claude Kirchner, A new equational unification method: a generalisation of Martelli-Montanari’s algorithm (pp. 224–247); Mark E. Stickel, A case study of theorem proving by the Knuth-Bendix method: discovering that \(x^ 3=x\) implies ring commutativity (pp. 248–258); L. Fribourg, A narrowing procedure for theories with constructors (pp. 259–281); Helene Kirchner, A general inductive completion algorithm and application to abstract data types (pp. 282–302);
Patrick Suppes, The next generation of interactive theorem provers (pp. 303–315); L. Wos, R. Veroff, B. Smith and W. McCune, The linked inference principle. II: The user’s viewpoint (pp. 316–332); Etienne Paul, A new interpretation of the resolution principle (pp. 333–355); David A. Plaisted, Using examples, case analysis, and dependency graphs in theorem proving (pp. 356–374); Dale A. Miller, Expansion tree proofs and their conversion to natural deduction proofs (pp. 375–393); Frank Pfenning, Analytic and nonanalytic proofs (pp. 394–413);
Jack Minker and Donald Perlis, Applications of protected circumscription (pp. 414–425); Kenneth Forsythe and Stanislaw Matwin, Implementation strategies for plan-based deduction (pp. 426–444); David A. Schmidt, A programming notation for tactical reasoning (pp. 445–459); Ketan Mulmuley, The mechanization of existence proofs of recursive predicates (pp. 460–475); Alex Pelin and Jean H. Gallier, Solving word problems in free algebras using complexity functions (pp. 476–495); Hans-Jurgen Ohlbach and Graham Wrightson, Solving a problem in relevance logic with an automated theorem prover (pp. 496–508).
The articles of this volume will be reviewed individually under the abbreviation ”Automated deduction, Proc. 7th int. Conf., Napa/Calif. 1984, Lect. Notes Comput. Sci. 170”.