Issue No.05 - May (1985 vol.11)
D.B. MacQueen , AT&T Bell Laboratories
Contrary to popular belief, equational logic with induction is not complete for initial models of equational specifications. Indeed, under some regimes (the Clear specification language and most other algebraic specification languages) no proof system exists which is complete even with respect to ground equations. A collection of known results is presented along with some new observations.
proof systems, Algebraic specifications, equational logic
D.B. MacQueen, "Completeness of Proof Systems for Equational Specifications", IEEE Transactions on Software Engineering, vol.11, no. 5, pp. 454-461, May 1985, doi:10.1109/TSE.1985.232484