書き換え帰納法に基づく帰納的定理の決定可能性
書誌事項
- タイトル別名
-
- Decidability of Inductive Theorems based on Rewriting Induction
説明
等式論理において，自然数やリストなどのデータ構造上で成立する等式を帰納的定理とよぶ．与えられた等式が等式論理の帰納的定理であるか否かは一般に決定不能であるが，いくつかの部分クラスに対する決定手続きが知られている．FalkeとKapur (2006)が与えた決定手続きは書き換え帰納法に基づく．一方，外山(2002)は，帰納的定理判定問題を2つの抽象リダクションシステムの等価性判定問題としてとらえることで，書き換え帰納法が帰納的定理の決定手続きとなるための十分条件を示した．しかし，この両者が保証している決定可能な帰納的定理のクラス間には包含関係がない．そこで，本論文ではこれら2つのアプローチを組み合わせることにより，従来保証されていた決定可能な帰納的定理のクラスを拡張する．
収録刊行物
-
- コンピュータ ソフトウェア
-
コンピュータ ソフトウェア 31 (3), 3_294-3_306, 2014
日本ソフトウェア科学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1390001204738467200
-
- NII論文ID
- 130004688287
-
- ISSN
- 02896540
-
- 本文言語コード
- ja
-
- 資料種別
- journal article
-
- データソース種別
-
- JaLC
- CiNii Articles
- KAKEN
-
- 抄録ライセンスフラグ
- 使用不可
