Abstract is missing.
- Using Meta-Theoretic Reasoning to do AlgebraLuigia Carlucci Aiello, Richard W. Weyhrauch. 1-13
- Generating Contours of Integration: An Application of Prolog in Symbolic ComputingGábor Belovári, J. A. Campbell. 14-23
- Using Meta-Level Inference for Selective Application of Multiple Rewrite Rules in Algebraic ManipulationAlan Bundy, Bob Welham. 24-38
- Proofs as Description of ComputationChris Goad. 39-52
- Program Synthesis from Incomplete SpecifiactionsGérard D. Guiho, Christian Gresse. 53-62
- A System for Proving Equivalences of Recursive ProgramsLaurent Kott. 63-69
- Variable Elimination and Chaining in a Resolution-based Prover for InequalitiesW. W. Bledsoe, Larry M. Hines. 70-87
- Decision Procedures for Some Fragments of Set TheoryAlfredo Ferro, Eugenio G. Omodeo, Jacob T. Schwartz. 88-96
- Simplifying Interpreted FormulasDonald W. Loveland, Robert E. Shostak. 97-109
- Specification and Verification of Real-Time, Distributed Systems Using the Theory of ConstraintsFrederick C. Furtek. 110-125
- Reasoning by Plausible InferenceLeonard Friedman. 126-142
- Logical Support in a Time-Varying ModelAlan M. Thompson. 143-153
- An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of ExpressionsPaul Y. Gloess. 154-169
- An Experiment with Edinburgh LCF Jacek Leszczylowski. 170-181
- An Approach to Theorem Proving on the Basis of a Typed Lambda-CalculusRob Nederpelt. 182-194
- Adding Dynamic Paramodulation to Rewrite AlgorithmsPaul Y. Gloess, Jean-Pierre H. Laurent. 195-207
- Hyperparamodulation: A Refinement of ParamodulationLarry Wos, Ross A. Overbeek, Lawrence J. Henschen. 208-219
- The AFFIRM Theorem Prover: Proof Forests and Management of Large ProofsRoddy W. Erickson, David R. Musser. 220-231
- Data Structures and Control Architectures for Implementation of Theorem-Proving ProgramsRoss A. Overbeek, Ewing L. Lusk. 232-249
- A Note on Resolution: How to Get Rid of Factoring without Loosing CompletenessHelga Noll. 250-263
- Abstraction Mappings in Mechanical Theorem ProvingDavid A. Plaisted. 264-280
- Transforming Matings into Natural Deduction ProofsPeter B. Andrews. 281-292
- Analysis of Dependencies to Improve the Behaviour of Logic ProgramsMaurice Bruynooghe. 293-305
- Selective Bachtracking for Logic ProgramsLuís Moniz Pereira, António Porto. 306-317
- Canonical Forms and UnificationJean-Marie Hullot. 318-334
- Deciding Unique Termination of Permutative Rewriting Systems: Choose Your Term Algebra CarefullyHans-Josef Jeanrond. 335-355
- How to Prove Algebraic Inductive Hypotheses Without InductionJoseph A. Goguen. 356-373
- A Complete, Nonredundant Algorithm for Reversed SkolemizationPhilip T. Cox, Tomasz Pietrzykowski. 374-385