Recognition of normal forms with tree automata for inductive theorem proving
Haruhiko Sato, Masahito Kurihara · Science and Information Conference · 2013
In this paper, we propose a method to construct a tree automata which recognizes all ground normal forms of a given term with respect to a terminating and confluent constructor TRS. We also show that the technique can be applied for generalization of conjecture in inductive theorem proving.