Automated Deduction
in Equational Logic and Cubic Curves

W. McCune and R. Padmanabhan

These web pages are a supplement to a monograph of the same name in Lecture Notes in Computer Science (AI subseries) #1095 Springer-Verlag, 1996. ISBN 3-540-61398-6.
The monograph can be ordered from Springer-Verlag. In the USA, the list price is $43; see Springer's New York web page or phone 1-800-777-4643. Outside the USA, the list price is DM 54,-; see Springer's web page in Germany or phone (49) 30 8207-0.

From the back cover of the book:

This monograph is the result of the cooperation of a mathematician, working in universal algebra and geometry, and a computer scientist, working in automated deduction: R. Padmanabhan contacted William McCune in order to find out whether the theorem prover Otter developed at Argonne National Laboratory could prove a few first-order theorems. Otter indeed succeeded and, in a few cases, even found slightly better results; this success was the starting point of a fruitful interdisciplinary joint effort.

This book is relevant for both mathematicians and computer scientists: mathematicians will find many new results in equational logic, universal algebra, and algebraic geometry and benefit from the start-of-the-art outline of the capabilities of automated deduction techniques; computer scientists interested in automated reasoning will find a large and varied source of theorems and problems that will be useful in designing and evaluating automated theorem proving systems and strategies.


  1. Introduction
  2. Otter and MACE
  3. Algebras Over Algebraic Curves
  4. Other (gL)-Algebras
  5. Semigroups
  6. Lattice-Like Algebras
  7. Independent Self-Dual Bases
  8. Miscellaneous Topics


Table of Contents

Input files and proofs