Abstract is missing.
- Universal UnificationJörg H. Siekmann. 1-42
- A Portable Environment for Research in Automated ReasoningEwing L. Lusk, Ross A. Overbeek. 43-52
- A Natural Proof System Based on rewriting TechniquesDeepak Kapur, Balakrishnan Krishnamurthy. 53-64
- EKL - A Mathematically Oriented Proof CheckerJussi Ketonen. 65-79
- A Linear Characterization of NP-Complete ProblemsSilvio Ursic. 80-100
- A Satisfiability Tester for Non-Clausal Propositional CalculusAllen Van Gelder. 101-112
- A Decision Method for Linear Temporal LogicAna R. Cavalli, Luis Fariñas del Cerro. 113-127
- A Progress Report on New Decision Algorithms for Finitely Prsented Abelian GroupsDallas Lankford, Gregory Butler II, A. Michael Ballantyne. 128-141
- Canonical Forms in Finitely Presented AlgebrasPhilippe le Chenadec. 142-165
- Term Rewriting Systems and AlgebraPierre Lescanne. 166-174
- Termination of a Set of Rules Modulo a Set of EquationsJean-Pierre Jouannaud, Miguel Munoz. 175-193
- Associative-Commutative UnificationFrançois Fages. 194-208
- A Linear Time Algorithm for a Subcase of Second Order InstantiationDonald Simon. 209-223
- A New Equational Unification Method: A Generalization of Martelli-Montanari s AlgorithmClaude Kirchner. 224-247
- A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring CommutativityMark E. Stickel. 248-258
- A Narrowing Procedure for Theories with ConstructorsLaurent Fribourg. 259-281
- A General Inductive Completion Algorithm and Application to Abstract Data TypesHélène Kirchner. 282-302
- The Next Generation of Interactive Theorem ProversPatrick Suppes. 303-315
- The Linked Inference Principle, II: The User s ViewpointLarry Wos, Robert Veroff, B. Smith, William McCune. 316-332
- A New Interpretation of the Resolution PrincipleEtienne Paul. 333-355
- Using Examples, Case Analysis, and Dependency Graphs in Theorem ProvingDavid A. Plaisted. 356-374
- Expansion Tree Proofs and Their Conversion to Natural Deduction ProofsDale Miller. 375-393
- Analytic and Non-analytic ProofsFrank Pfenning. 394-413
- Applications of Protected CircumscriptionJack Minker, Donald Perlis. 414-425
- Implementation Strategies for Plan-Based DeductionKenneth Forsythe, Stan Matwin. 426-444
- A Programming Notation for Tactical ReasoningDavid A. Schmidt. 445-459
- The Mechanization of Existence Proofs of Recursive PredicatesKetan Mulmuley. 460-475
- Solving Word Problems in Free Algebras Using Complexity FunctionsAlex Pelin, Jean H. Gallier. 476-495
- Solving a Problem in Relevance Logic with an Automated Theorem ProverHans Jürgen Ohlbach, Graham Wrightson. 496-508