Title :
Completeness of Proof Systems for Equational Specifications
Author :
Macqueen, David B. ; Sannella, Donald T.
Author_Institution :
AT&T Bell Laboratories
fDate :
5/1/1985 12:00:00 AM
Abstract :
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.
Keywords :
Algebraic specifications; equational logic; proof systems; Algebra; Artificial intelligence; Automatic logic units; Computer science; Councils; Equations; Logic functions; Specification languages; Algebraic specifications; equational logic; proof systems;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.1985.232484
