Completeness of Proof Systems for Equational Specifications
David B. MacQueen, Donald Sannella · IEEE Transactions on Software Engineering · 1985
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.