## Robert E. Shostak

*Proceedings of the Seventh International Conference on Automated Deduction*

CADE, 1984.

@proceedings{CADE-1984, address = "Napa, California, USA", editor = "Robert E. Shostak", isbn = "3-540-96022-8", publisher = "{Springer-Verlag}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the Seventh International Conference on Automated Deduction}", volume = 170, year = 1984, }

### Contents (29 items)

- CADE-1984-Siekmann #unification
- Universal Unification (JHS), pp. 1–42.
- CADE-1984-LuskO #automation #reasoning #research
- A Portable Environment for Research in Automated Reasoning (ELL, RAO), pp. 43–52.
- CADE-1984-KapurK #proving
- A Natural Proof System Based on rewriting Techniques (DK, BK), pp. 53–64.
- CADE-1984-Ketonen #named #proving
- EKL — A Mathematically Oriented Proof Checker (JK), pp. 65–79.
- CADE-1984-Ursic #linear #problem
- A Linear Characterization of NP-Complete Problems (SU), pp. 80–100.
- CADE-1984-Gelder #calculus #satisfiability
- A Satisfiability Tester for Non-Clausal Propositional Calculus (AVG), pp. 101–112.
- CADE-1984-CavalliC #linear #logic
- A Decision Method for Linear Temporal Logic (ARC, LFdC), pp. 113–127.
- CADE-1984-LankfordBB #algorithm
- A Progress Report on New Decision Algorithms for Finitely Prsented Abelian Groups (DL, GBI, AMB), pp. 128–141.
- CADE-1984-Chenadec #algebra #canonical
- Canonical Forms in Finitely Presented Algebras (PlC), pp. 142–165.
- CADE-1984-Lescanne #algebra #term rewriting
- Term Rewriting Systems and Algebra (PL), pp. 166–174.
- CADE-1984-JouannaudM #equation #set #termination
- Termination of a Set of Rules Modulo a Set of Equations (JPJ, MM), pp. 175–193.
- CADE-1984-Fages #commutative #unification
- Associative-Commutative Unification (FF), pp. 194–208.
- CADE-1984-Simon #algorithm #higher-order #linear
- A Linear Time Algorithm for a Subcase of Second Order Instantiation (DS), pp. 209–223.
- CADE-1984-Kirchner #algorithm #equation #unification
- A New Equational Unification Method: A Generalization of Martelli-Montanari’s Algorithm (CK), pp. 224–247.
- CADE-1984-Stickel #case study #commutative #proving #theorem proving
- A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity (MES), pp. 248–258.
- CADE-1984-Fribourg
- A Narrowing Procedure for Theories with Constructors (LF), pp. 259–281.
- CADE-1984-Kirchner84a #algorithm #data type #induction
- A General Inductive Completion Algorithm and Application to Abstract Data Types (HK), pp. 282–302.
- CADE-1984-Suppes #generative #interactive #proving #theorem proving
- The Next Generation of Interactive Theorem Provers (PS), pp. 303–315.
- CADE-1984-WosVSM
- The Linked Inference Principle, II: The User’s Viewpoint (LW, RV, BS, WM), pp. 316–332.
- CADE-1984-Paul #principle
- A New Interpretation of the Resolution Principle (EP), pp. 333–355.
- CADE-1984-Plaisted #analysis #dependence #graph #proving #theorem proving #using
- Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving (DAP), pp. 356–374.
- CADE-1984-Miller #deduction #proving
- Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs (DM), pp. 375–393.
- CADE-1984-Pfenning #proving
- Analytic and Non-analytic Proofs (FP), pp. 394–413.
- CADE-1984-MinkerP
- Applications of Protected Circumscription (JM, DP), pp. 414–425.
- CADE-1984-ForsytheM #deduction #implementation
- Implementation Strategies for Plan-Based Deduction (KF, SM), pp. 426–444.
- CADE-1984-Schmidt #programming #reasoning
- A Programming Notation for Tactical Reasoning (DAS), pp. 445–459.
- CADE-1984-Mulmuley #proving #recursion
- The Mechanization of Existence Proofs of Recursive Predicates (KM), pp. 460–475.
- CADE-1984-PelinG #algebra #complexity #problem #using #word
- Solving Word Problems in Free Algebras Using Complexity Functions (AP, JHG), pp. 476–495.
- CADE-1984-OhlbachW #automation #logic #problem #proving #theorem proving
- Solving a Problem in Relevance Logic with an Automated Theorem Prover (HJO, GW), pp. 496–508.

9 ×#proving

4 ×#algorithm

4 ×#theorem proving

3 ×#algebra

3 ×#linear

3 ×#problem

3 ×#unification

2 ×#automation

2 ×#commutative

2 ×#deduction

4 ×#algorithm

4 ×#theorem proving

3 ×#algebra

3 ×#linear

3 ×#problem

3 ×#unification

2 ×#automation

2 ×#commutative

2 ×#deduction