帰納的定理の決定可能なクラスについて
スポンサーリンク
概要
- 論文の詳細を見る
項書換え系における帰納的定理の自動証明が決定可能である条件を特徴づけるために, GieslとKapurは被覆証明可能というクラスを提案した.これは, 被覆証明帰納法を用いたときに, 必ず帰納的定理が決定可能となる等式の集合である.しかし, このクラスは項書換え系の各ルールの左辺と右辺に現れる定義関数記号が同じでなければならないという制限がある.本論文では, 被覆集合の概念を拡張し, 項書換え系のルールの左辺と右辺に異なる定義関数記号が含まれている場合も許した被覆証明可能であるクラスを特徴づける.また, 被覆証明可能であるための構文的な十分条件を与える.
- 社団法人電子情報通信学会の論文
- 2002-01-23
著者
関連論文
- 帰納的定理の決定可能なクラスについて
- 項書き換えシステムの合流性自動判定
- A-033 S式書き換えシステムの停止性を保証するカリー化について(モデル・アルゴリズム・プログラミング,一般論文)
- 木準同型写像を用いた項パターンマッチング
- 反証機能付き書き換え帰納法のための補題自動生成法
- 新しいソフトウェアの実現 : 科研「情報学」プロジェクトA01柱を振り返って(「情報学を創る」-科研プロジェクトがめざしたもの)
- LA-009 項書き換えシステムの合流性自動判定(モデル・アルゴリズム・プログラミング)
- LA-002 パターンに基づくプログラム変換における列変数の導入(A分野:モデル・アルゴリズム・プログラミング)
- A-032 多重Knuth-Bendix完備化における危険対除去手法の導入(モデル・アルゴリズム・プログラミング,一般論文)
- A-034 基底項書き換え系の合流性自動判定(モデル・アルゴリズム・プログラミング,一般論文)
- 修正AC単調意味論経路順序によるAC停止性
- 修正AC単調意味論経路順序によるAC停止性
- 優先順序付き書き換えの計算モデル