On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms

Naoki Nishida
(Nagoya University)
Masahiko Sakai
(Nagoya University)
Yasuhiro Nakano
(Nagoya University)

An inductive theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision procedure for reduction-completeness of constrained terms. In addition, the sufficient complete property of constrained term rewriting systems enables us to relax the side conditions of some inference rules in the proving method. These two properties can be reduced to intersection emptiness problems related to sets of ground instances for constrained terms. This paper proposes a method to construct deterministic, complete, and constraint-complete constrained tree automata recognizing ground instances of constrained terms.

In Sebastian Maneth: Proceedings Second International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2013), Hanoi, Vietnam, 19/10/2013, Electronic Proceedings in Theoretical Computer Science 134, pp. 1–10.
Published: 20th November 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.134.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org