制約付き項のインスタンスを受理する制約付き木オートマトンの構成法

機関リポジトリ HANDLE Web Site オープンアクセス

書誌事項

タイトル別名
  • セイヤク ツキ コウ ノ インスタンス オ ジュリ スル セイヤク ツキ キオートマトン ノ コウセイホウ
  • Construction of Constrained Tree Automata Recognizing Ground Instances of Constrained Terms

この論文をさがす

抄録

制約付き項書換え系の書換え帰納法に基づいた定理自動証明の際に、制約付き項書換え系のR完全性の判定手続きが必要である。また、対象の制約付き項書換え系が十分完全性を持つ場合に、定理自動証明中の推論規則の適用条件を緩和することができる。これらの性質は、制約付き項のインスタンスの集合に関する積集合空問題に帰着できる。本論文では、制約付き項のインスタンスを受理する制約付き木オートマトンの構成法を提案する。さらに、制約付き木オートマトン中でどの入力基底項も到達することのない状態を削除する手法を提案することで、R完全性や十分完全性の判定の精度向上と効率化をめざす。

収録刊行物

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ