Proceedings of the Seventh International Conference on Automated Deduction
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

Robert E. Shostak
Proceedings of the Seventh International Conference on Automated Deduction
CADE, 1984.

TEST
DBLP
Scholar
Full names Links ISxN
@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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.