Theorem Proving and Algebra book (2006) [pdf]

[Submitted on 7 Jan 2021 (v1), last revised 16 Jan 2021 (this version, v2)]

Abstract: This book can be seen either as a text on theorem proving that uses
techniques from general algebra, or else as a text on general algebra
illustrated and made concrete by practical exercises in theorem proving. The
book considers several different logical systems, including first-order logic,
Horn clause logic, equational logic, and first-order logic with equality.
Similarly, several different proof paradigms are considered. However, we do
emphasize equational logic, and for simplicity we use only the OBJ3 software
system, though it is used in a rather flexible manner. We do not pursue the
lofty goal of mechanizing proofs like those of which mathematicians are justly
so proud; instead, we seek to take steps towards providing mechanical
assistance for proofs that are useful for computer scientists in developing
software and hardware. This more modest goal has the advantage of both being
achievable and having practical benefits.

The following topics are covered: many-sorted signature, algebra and
homomorphism; term algebra and substitution; equation and satisfaction;
conditional equations; equational deduction and its completeness; deduction for
conditional equations; the theorem of constants; interpretation and equivalence
of theories; term rewriting, termination, confluence and normal form; abstract
rewrite systems; standard models, abstract data types, initiality, and
induction; rewriting and deduction modulo equations; first-order logic, models,
and proof planning; second-order algebra; order-sorted algebra and rewriting;
modules; unification and completion; and hidden algebra. In parallel with these
are a gradual introduction to OBJ3, applications to group theory, various
abstract data types (such as number systems, lists, and stacks), propositional
calculus, hardware verification, the {lambda}-calculus, correctness of
functional programs, and other topics.