制約付き木オートマトンとその間包性

摘要

木オートマトンは項を入力としたオートマトンであり，和集合·補集合·積集合演算に閉じていることや空判定問題が決定可能であることから，項書換え系の性質を調べることに有効である．また，近年，制約付き項書換え系に関する研究が行われており，特に定理自動証明の研究が注目されている．本稿では，等号不等号制約付き木オートマトンの制約を任意の制約系を指定できるように一般化した制約付き木オートマトンを提案し，任意の制約付き木オートマトンに対して決定性と完全性を持ち受理集合が等価である制約付き木オートマトンが存在することを示す．さらに，制約付き木オートマトンのクラスが和·積·補集合演算に閉じていることを示す．