7th International Conference on Automated Deduction

Universal Unification.- A Portable Environment for Research in Automated Reasoning.- A Natural Proof System Based on Rewriting Techniques.- EKL-A Mathematically Oriented Proof Checker.- A Linear Characterization of NP-Complete Problems.- A Satisfiability Tester for Non-Clausal Propositional Calculus.- A Decision Method for Linear Temporal Logic.- A Progress Report on New Decision Algorithms for Finitely Presented Abelian Groups.- Canonical Forms in Finitely Presented Algebras.- Term Rewriting Systems and Algebra.- Termination of a Set of Rules Modulo a Set of Equations.- Associative-Commutative Unification.- A Linear Time Algorithm for a Subcase of Second Order Instantiation.- A New Equational Unification Method: A Generalisation of Martelli-Montanari's Algorithm.- A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x 3 = x Implies Ring Commutativity.- A Narrowing Procedure for Theories with Constructors.- A General Inductive Completion Algorithm and Application to Abstract Data Types.- The Next Generation of Interactive Theorem Provers.- The Linked Inference Principle, II: The User's Viewpoint.- A New Interpretation of the Resolution Principle.- Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving.- Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs.- Analytic and Non-analytic Proofs.- Applications of Protected Circumscription.- Implementation Strategies for Plan-Based Deduction.- A Programming Notation for Tactical Reasoning.- The Mechanization of Existence Proofs of Recursive Predicates.- Solving Word Problems in Free Algebras Using Complexity Functions.- Solving a Problem in Relevance Logic with an Automated Theorem Prover.