Automation of Reasoning

Automated Theorem Proving 1965-1970.- 1967.- A Cancellation Algorithm for Elementary Logic.- An Inverse Method for Establishing Deducibility of Nonprenex Formulas of the Predicate Calculus.- Automatic Theorem Proving With Renamable and Semantic Resolution.- The Concept of Demodulation in Theorem Proving.- 1968.- Resolution with Merging.- On Simplifying the Matrix of a WFF.- Mechanical Theorem-Proving by Model Elimination.- The Generalized Resolution Principle.- New Directions in Mechanical Theorem Proving.- Automath, a Language for Mathematics.- 1969.- Semi-Automated Mathematics.- Semantic Trees in Automatic Theorem-Proving.- A Simplified Format for the Model Elimination Theorem-Proving Procedure.- Theorem-Provers Combining Model Elimination and Resolution.- Relationship between Tactics of the Inverse Method and the Resolution Method.- E-Resolution: Extension of Resolution to Include the Equality Relation.- 1969.- Advances and Problems in Mechanical Proof Procedures.- Paramodulation and Theorem-Proving in First-Order Theories with Equality.- 1970.- Completeness Results for E-Resolution.- A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness.- The Unit Proof and the Input Proof in Theorem Proving.- Simple Word Problems in Universal Algebras.- The Case for Using Equality Axioms in Automatic Demonstration.- A Linear Format for Resolution.- An Interactive Theorem-Proving Program.- Refinement Theorems in Resolution Theory.- On the Complexity of Derivation in Propositional Calculus.- After 1970.- Resolution in Type Theory.- Splitting and Reduction Heuristics in Automatic Theorem Proving.- A Computer Algorithm for the Determination of Deducibility on the Basis of the Inverse Method.- Linear Resolution with Selection Function.- MaximalModels and Refutation Completeness: Semidecision Procedures in Automatic Theorem Proving.- Bibliography on Computational Logic.