Introducing CafeOBJ (3) : Equational Reasoning and Term Rewriting Systems
-
- 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
Abstract
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
- Tweet
Details
-
- CRID
- 1390282679714986624
-
- NII Article ID
- 110006840405
-
- NII Book ID
- AN10075819
-
- NDL BIB ID
- 9599985
-
- ISSN
- 02896540
-
- Web Site
- http://hdl.handle.net/2297/12395
-
- Text Lang
- ja
-
- Data Source
-
- JaLC
- IRDB
- NDL
- CiNii Articles
- KAKEN
-
- Abstract License Flag
- Disallowed