On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms

Autor:	Naoki Nishida, Masahiko Sakai, Yasuhiro Nakano
Jazyk:	angličtina
Rok vydání:	2013
Předmět:	Mathematics QA1-939 Electronic computers. Computer science QA75.5-76.95
Zdroj:	Electronic Proceedings in Theoretical Computer Science, Vol 134, Iss Proc. TTATT 2013, Pp 1-10 (2013)
Druh dokumentu:	article
ISSN:	2075-2180 86584316
DOI:	10.4204/EPTCS.134.1
Popis:	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.
Databáze:	Directory of Open Access Journals
Externí odkaz:	https://doaj.org/article/25fa60ed8658431688b19cde85019fd6 Zobrazit plný text záznamu View record in DOAJ