制約付き項のインスタンスを受理する制約付き木オートマトンの構成法(論理と形式手法)

スポンサーリンク

概要

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

著者

関連論文

もっと見る

スポンサーリンク