文献

J-GLOBAL ID：201502257581879059   整理番号：15A0582392

構成子に基づく順序ソートパラメータ化仕様の十分完全性について

Sufficient completeness of constructor-based order-sorted parameterized specifications

著者 (4件)： 中村正樹 (富山県大) ,  GAINA Daniel Mircea (北陸先端科学技術大学院大) ,  緒方和博 (北陸先端科学技術大学院大) ,  二木厚吉 (北陸先端科学技術大学院大)
資料名： 電子情報通信学会技術研究報告  (IEICE Technical Report (Institute of Electronics, Information and Communication Engineers))
巻： 114  号： 510(SS2014 55-73)  ページ： 1-6  発行年： 2015年03月02日 
JST資料番号： S0532B  ISSN： 0913-5685  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 代数仕様言語CafeOBJでは,構成子に基づく順序ソート(CBOS)代数をモデルに持つ仕様を記述できる。また,パラメータ機構を持ったパラメータ化仕様も記述できる。代数仕様の十分完全性は,演算子のwell-defined性を保証する重要な性質であり,CBOS仕様においても始モデルの存在を保証する重要な性質である。代数仕様の十分完全性は,一般には決定不能であるが,項書き換えシステムによる証明手法が知られている。本論文では,CBOSパラメータ化仕様を対象とし,項書き換え理論に基づくパラメータ化仕様の具象仕様が十分完全性を満たすための十分条件を与える。(著者抄録)

シソーラス用語： *仕様 ,  仕様記述言語 ,  ソーティング ,  *十分条件 ,  *完全性 ,  パラメタリゼーション ,  演算子 ,  項書換え系 ,  順序 ,  証明
準シソーラス用語： ソート ,  パラメータ化 ,  項書換えシステム ,  仕様言語 ,  *代数仕様

分類 (2件)： 人工知能  (JE08000Z) ,  計算機システム開発  (JD02010R)

引用文献 (11件)：

• CafeOBJ. http://www.ldl.jaist.ac.jp/cafeobj/.
• Razvan Diaconescu and Kokichi Futatsugi. CafeOBJ Report. World Scientific, 1998.
• Kokichi Futatsugi, Daniel Găineă, and Kazuhiro Ogata. Principles of proof scores in CafeOBJ. Theor. Comput. Sci., 464:90-112, December 2012.
• Daniel Găină and Kokichi Futatsugi. Initial semantics in logics with constructors. Journal of Logic and Computation, 2012. doi: 10.1093/logcom/exs044.
• Deepak Kapur, Paliath Narendran, Daniel J. Rosenkrantz, and Hantao Zhang. Sufficient-completeness, groundreducibility and their complexity. Acta Inf., 28(4):311-350, April 1991.

タイトルに関連する用語 (5件)： 順序 ,  ソート ,  パラメータ化 ,  仕様 ,  完全性