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)

9 ×#proving
4 ×#algorithm
4 ×#theorem proving
3 ×#algebra
3 ×#linear
3 ×#problem
3 ×#unification
2 ×#automation
2 ×#commutative
2 ×#deduction

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.