Theorem Proving and Algebra

To be published by MIT Press, someday. This draft textbook is intended to introduce general (universal) algebra and its applications to computer science, especially to theorem proving.

The following parts are available:

Introduction, Chapter 1.
First Order Logic, Chapter 8, an algebraic formulation of first order logic, slanted towards applications to proof planning.
References.

This is still a draft of the book, and your comments are very welcome!

Table of Contents

1. Introduction. 2. Signature and Algebra. 3. Homomorphism, Equation and Satisfaction. 4. Equational Deduction. 5. Rewriting. 6. Deduction and Rewriting Modulo Equations. 7. Standard Models, Initial Models and Induction. 8. First Order Logic and Proof Planning. 9. Second Order Equational Logic. 10. Order Sorted Algebra. 11. Generic Modules. 12. Unification. 13. Hidden Algebra. 14. A General Framework. A. OBJ3 Syntax and Usage. B. Exiled Proofs. C. Some Background on Relations. D. Social Implications.

Back to my homepage

18 April 1997