Handbook of Automated Reasoning

Preface

Automated reasoning has matured into one of the most advanced areas of computer science. During the half-century since the pioneering publications of the 1950s, significant progress has been achieved both in its theory and practice, culminating in a completely automatic solution of the Robbins Problem by the theorem prover EQP implemented by Bill McCune. This problem in algebra had remained open for over 50 years despite repeated attempts of mathematicians to solve it.

Several theoretical results, ideas, and techniques contributed to the Robbins Problem solution. We mention only a few: equational unification, and in particular AC-unification (Chapter 8 of this Handbook), completion procedures and notions of redundancy (Chapters 2 ...