Handbook of Automated Reasoning

Chapter 1

The Early History of Automated Deduction: Dedicated to the memory of Hao Wang

Martin Davis

Contents

1  Presburger's Procedure   5

2  Newell, Shaw & Simon, and H. Gelernter   6

3  First-Order Logic   7

Bibliography   12

Index   15

With the ready availability of serious computer power, deductive reasoning, especially as embodied in mathematics, presented an ideal target for those interested in experimenting with computer programs that purported to implement the “higher” human faculties. This was because mathematical reasoning combines objectivity with creativity in a way difficult to find in other domains. For this endeavor, two paths presented themselves. One was to try to understand what people do when they create ...