Automation of Reasoning

The Prehistory and Early History of Automated Deduction.- Mechanical Proof Search and the Theory of Logical Deduction in the USSR.- 1957.- A Computer Program for Presburger's Algorithm.- Empirical Explorations with the Logic Theory Machine: A Case Study in Heuristics.- Proving a Theorem (as Done by Man, Logician or Machine).- 1958.- On Machines Which Prove Theorems.- 1959.- A non-heuristic Program for Proving Elementary Logical Theorems.- Realization of a Geometry-Theorem Proving Machine.- 1960.- A Computing Procedure for Quantification Theory.- Empirical Explorations of the Geometry-Theorem Proving Machine.- A Proof Method for Quantification Theory: Its Justification and Realization.- An Improved Proof Procedure.- A Mechanical Proof Procedure and its Realization in an Electronic Computer.- Proving Theorems by Pattern Recognition.- Toward Mechical Mathematics.- 1962.- A Machine Program for Theorem Proving.- Theorem Testing by Computer.- Exploratory Mathematics by Machine.- Machine-Generated Problem-Solving Graphs.- 1963.- Eliminating the Irrelevant from Mechanical Proofs.- A Semi-Decision Procedure for the Functional Calculus.- A Computer Program for a Solvable Case of the Decision Problem.- A Simplified Proof Method for Elementary Logic.- Theorem-Proving on the Computer.- 1964.- The Unit Preference Strategy in Theorem Proving.- 1965.- A Machine Oriented Logic Based on the Resolution Principle.- Automatic Deduction with Hyper-Resolution.- An Algorithm for a Machine Search of a Natural Logical Deduction in a Propositional Calculus.- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving.- 1966.- Theorem-Proving for Computers: Some Results on Resolution and Renaming.- Bibliography on Computational Logic.