CMU 15-671Models of Software SystemsFall 1995
Equational Reasoning
Garlan & Wing Handout 2 11 September 1995
There is a very simple, but powerful subset of first-order predicate logic called equational logic. This handout explains the essence of equational logic and equational-style proofs and how they are relevant to software engineering.
In this handout and the next I will be copying examples and statements verbatim (or nearly so) from Gries and Schneider's book, A Logical Approach to Discrete Math, Springer-Verlag, 1993. When I do, I'll reference it as [GS].