Introducing CafeOBJ (3) : Equational Reasoning and Term Rewriting Systems

DOI IR IR (HANDLE) Web Site 7 References
  • NAKAMURA Masaki
    School of Electrical and Computer Engineering, Kanazawa University
  • FUTATSUGI Kokichi
    Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
  • OGATA Kazuhiro
    Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)

Bibliographic Information

Other Title
  • ＣａｆｅＯＢＪ入門（３）等式推論と項書換システム
  • チュートリアル CafeOBJ入門(3)等式推論と項書換システム
  • チュートリアル CafeOBJ ニュウモン 3 トウシキ スイロン ト コウ カキカエ システム

Search this article

Description

Equational inference is the most fundamental inference mechanism for CafeOBJ algebraic specification language. Term rewriting system can realize equational inference in an efficient way. Several pieces of fundamental knowledge on term rewriting systems, which are valuable for CafeOBJ specification development, are described. We present the ways to describe specifications which satisfies fundamental properties of term rewriting systems: termination, confluence and sufficient completeness properties, and also discuss about applications to specifications including associative and/or commutative operators, conditional equations, and so on.

Journal

  • Computer Software

    Computer Software 25 (3), 69-80, 2008

    Japan Society for Software Science and Technology

References(7)*help

See more

Related Projects

See more

Details 詳細情報について

Report a problem

Back to top