Automated Deduction
in Equational Logic and Cubic Curves
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.
Chapters
- Introduction
- Otter and MACE
- Algebras Over Algebraic Curves
- Other (gL)-Algebras
- Semigroups
- Lattice-Like Algebras
- Independent Self-Dual Bases
- Miscellaneous Topics
Appendices
- A. Summary of Theorems Proved
- B. Open Questions
- C. Otter's Autonomous Mode