Handbook of Automated Reasoning

Table of Contents

Cover image

Title page

Copyright page

Preface

List of Contributors

List of Second Readers

Volume 1.

 

Part I: History

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

1 Presburger's Procedure

2 Newell, Shaw & Simon, and H. Gelernter

3 First-Order Logic

Index

Part II: Classical Logic

Chapter 2: Resolution Theorem Proving

1 Introduction

2 Preliminaries

3 Standard Resolution

4 A Framework for Saturation-Based Theorem Proving

5 General Resolution

6 Basic Resolution Strategies

7 Refined Techniques for Defining Orderings and Selection Functions

8 Global Theorem Proving Methods

9 First-Order Resolution Methods

10 Effective Saturation of First-Order Theories

11 Concluding Remarks

Acknowledgments ...