default search action
7th CADE 1984: Napa, California, USA
- Robert E. Shostak:
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. M. 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, Barry 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-18 18:34 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: