• DocumentCode
    1237857
  • Title

    Completeness of Proof Systems for Equational Specifications

  • Author

    Macqueen, David B. ; Sannella, Donald T.

  • Author_Institution
    AT&T Bell Laboratories
  • Issue
    5
  • fYear
    1985
  • fDate
    5/1/1985 12:00:00 AM
  • Firstpage
    454
  • Lastpage
    461
  • 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;
  • fLanguage
    English
  • Journal_Title
    Software Engineering, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0098-5589
  • Type

    jour

  • DOI
    10.1109/TSE.1985.232484
  • Filename
    1702035