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

制約付き項書換え系の書換え帰納法に基づいた定理自動証明の際に、制約付き項書換え系のR完全性の判定手続きが必要である。また、対象の制約付き項書換え系が十分完全性を持つ場合に、定理自動証明中の推論規則の適用条件を緩和することができる。これらの性質は、制約付き項のインスタンスの集合に関する積集合空問題に帰着できる。本論文では、制約付き項のインスタンスを受理する制約付き木オートマトンの構成法を提案する。さらに、制約付き木オートマトン中でどの入力基底項も到達することのない状態を削除する手法を提案することで、R完全性や十分完全性の判定の精度向上と効率化をめざす。
A theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision procedure for R-completeness of constrained term rewriting systems. In addition, sufficient completeness of constrained term rewriting systems enables us to relax the side conditions of some inference rules in the proving method. These two properties of constrained term rewriting systems can be reduced to intersection emptiness problems related to sets of ground instances for constrained terms. In this paper, we propose a method to construct constrained tree automata recognizing ground instances of constrained terms. We also propose a method to remove states from a constrained tree automaton, to which no ground term transitions, thus improving the accuracy for the judgements of R-completeness and sufficient completeness.
IEICE Technical Report;SS2012-47