7. CADE 1984: Napa, California, USA

Robert E. Shostak (Ed.): 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings. Lecture Notes in Computer Science 170 Springer 1984, ISBN 3-540-96022-8

Monday Morning

Jörg H. Siekmann:
Universal Unification. 1-42
Ewing L. Lusk, Ross A. Overbeek:
A Portable Environment for Research in Automated Reasoning. 43-52
Deepak Kapur, Balakrishnan Krishnamurthy:
A Natural Proof System Based on rewriting Techniques. 53-64
Jussi Ketonen:
EKL - A Mathematically Oriented Proof Checker. 65-79

Monday Afternoon

Silvio Ursic:
A Linear Characterization of NP-Complete Problems. 80-100
Allen Van Gelder:
A Satisfiability Tester for Non-Clausal Propositional Calculus. 101-112
Ana R. Cavalli, Luis Fariñas del Cerro:
A Decision Method for Linear Temporal Logic. 113-127
Dallas Lankford, Gregory Butler II, A. Michael Ballantyne:
A Progress Report on New Decision Algorithms for Finitely Prsented Abelian Groups. 128-141
Philippe le Chenadec:
Canonical Forms in Finitely Presented Algebras. 142-165
Pierre Lescanne:
Term Rewriting Systems and Algebra. 166-174
Jean-Pierre Jouannaud, Miguel Munoz:
Termination of a Set of Rules Modulo a Set of Equations. 175-193

Tuesday Morning

François Fages:
Associative-Commutative Unification. 194-208
Donald Simon:
A Linear Time Algorithm for a Subcase of Second Order Instantiation. 209-223
Claude Kirchner:
A New Equational Unification Method: A Generalization of Martelli-Montanari's Algorithm. 224-247
Mark E. Stickel:
A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity. 248-258
Laurent Fribourg:
A Narrowing Procedure for Theories with Constructors. 259-281
Hélène Kirchner:
A General Inductive Completion Algorithm and Application to Abstract Data Types. 282-302

Tuesday Evening

Patrick Suppes:
The Next Generation of Interactive Theorem Provers. 303-315

Wednesday Morning

Larry Wos, Robert Veroff, B. Smith, William McCune:
The Linked Inference Principle, II: The User's Viewpoint. 316-332
Etienne Paul:
A New Interpretation of the Resolution Principle. 333-355
David A. Plaisted:
Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving. 356-374
Dale Miller:
Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. 375-393
Frank Pfenning:
Analytic and Non-analytic Proofs. 394-413

Wednesday Afternoon

Jack Minker, Donald Perlis:
Applications of Protected Circumscription. 414-425
Kenneth Forsythe, Stan Matwin:
Implementation Strategies for Plan-Based Deduction. 426-444
David A. Schmidt:
A Programming Notation for Tactical Reasoning. 445-459
Ketan Mulmuley:
The Mechanization of Existence Proofs of Recursive Predicates. 460-475
Alex Pelin, Jean H. Gallier:
Solving Word Problems in Free Algebras Using Complexity Functions. 476-495
Hans Jürgen Ohlbach, Graham Wrightson:
Solving a Problem in Relevance Logic with an Automated Theorem Prover. 496-508