7th International Conference on Automated Deduction

1. Front Matter

   Pages i-viii

   PDF

2. Universal Unification

   • Jörg H. Siekmann

   Pages 1-42

3. A Portable Environment for Research in Automated Reasoning

   • Ewing L. Lusk, Ross A. Overbeek

   Pages 43-52

4. A Natural Proof System Based on Rewriting Techniques

   • Deepak Kapur, Balakrishnan Krishnamurthy

   Pages 53-64

5. EKL—A Mathematically Oriented Proof Checker

   • Jussi Ketonen

   Pages 65-79

6. A Linear Characterization of NP-Complete Problems

   • Silvio Ursic

   Pages 80-100

7. A Satisfiability Tester for Non-Clausal Propositional Calculus

   • Allen Van Gelder

   Pages 101-112

8. A Decision Method for Linear Temporal Logic

   • Ana R. Cavalli, Luis FariÑas Del Cerro

   Pages 113-127

9. A Progress Report on New Decision Algorithms for Finitely Presented Abelian Groups

   • D. Lankford, G. Butler, A. Ballantyne

   Pages 128-141

10. Canonical Forms in Finitely Presented Algebras

    • Philippe Le Chenadec

    Pages 142-165

11. Term Rewriting Systems and Algebra

    • Pierre Lescanne

    Pages 166-174

12. Termination of a Set of Rules Modulo a Set of Equations

    • Jean-Pierre Jouannaud, Miguel Munoz

    Pages 175-193

13. Associative-Commutative Unification

    • François Fages

    Pages 194-208

14. A Linear Time Algorithm for a Subcase of Second Order Instantiation

    • Donald Simon

    Pages 209-223

15. A New Equational Unification Method: A Generalisation of Martelli-Montanari’s Algorithm

    • Claude Kirchner

    Pages 224-247

16. A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x ³ = x Implies Ring Commutativity

    • Mark E. Stickel

    Pages 248-258

17. A Narrowing Procedure for Theories with Constructors

    • L. Fribourg

    Pages 259-281

18. A General Inductive Completion Algorithm and Application to Abstract Data Types

    • Helene Kirchner

    Pages 282-302

19. The Next Generation of Interactive Theorem Provers

    • Patrick Suppes

    Pages 303-315

20. The Linked Inference Principle, II: The User’s Viewpoint

    • L. Wos, R. Veroff, B. Smith, W. McCune

    Pages 316-332

The Seventh International Conference on Automated Deduction was held May 14-16, 19S4, in Napa, California. The conference is the primary forum for reporting research in all aspects of automated deduction, including the design, implementation, and applications of theorem-proving systems, knowledge representation and retrieval, program verification, logic programming, formal specification, program synthesis, and related areas. The presented papers include 27 selected by the program committee, an invited keynote address by Jorg Siekmann, and an invited banquet address by Patrick Suppes. Contributions were presented by authors from Canada, France, Spain, the United Kingdom , the United States, and West Germany. The first conference in this series was held a decade earlier in Argonne, Illinois. Following the Argonne conference were meetings in Oberwolfach, West Germany (1976), Cambridge, Massachusetts (1977), Austin, Texas (1979), Les Arcs, France (19S0), and New York, New York (19S2). Program Committee P. Andrews (CMU) W.W. Bledsoe (U. Texas) past chairman L. Henschen (Northwestern) G. Huet (INRIA) D. Loveland (Duke) past chairman R. Milner (Edinburgh) R. Overbeek (Argonne) T. Pietrzykowski (Acadia) D. Plaisted (U. Illinois) V. Pratt (Stanford) R. Shostak (SRI) chairman J. Siekmann (U. Kaiserslautern) R. Waldinger (SRI) Local Arrangements R. Schwartz (SRI) iv CONTENTS Monday Morning Universal Unification (Keynote Address) Jorg H. Siekmann (FRG) .

• Theorembeweisen (Kybern.)
• automated deduction
• automated reasoning
• commutative property
• complexity
• knowledge representation
• proof
• proving
• verification

• SRI International, Menlo Park, USA

  R. E. Shostak

Policies and ethics