On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms

On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms

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 s...

Full description

Bibliographic Details
Main Authors: Naoki Nishida, Masahiko Sakai, Yasuhiro Nakano
Format: Article
Language:English
Published: Open Publishing Association 2013-11-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1311.5567v1
id doaj-25fa60ed8658431688b19cde85019fd6
record_format Article
spelling doaj-25fa60ed8658431688b19cde85019fd62020-11-24T23:16:50ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-11-01134Proc. TTATT 201311010.4204/EPTCS.134.1:3On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained TermsNaoki Nishida0Masahiko Sakai1Yasuhiro Nakano2 Nagoya University Nagoya University 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.http://arxiv.org/pdf/1311.5567v1
collection DOAJ
language English
format Article
sources DOAJ
author Naoki Nishida
Masahiko Sakai
Yasuhiro Nakano
spellingShingle Naoki Nishida
Masahiko Sakai
Yasuhiro Nakano
On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms
Electronic Proceedings in Theoretical Computer Science
author_facet Naoki Nishida
Masahiko Sakai
Yasuhiro Nakano
author_sort Naoki Nishida
title On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms
title_short On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms
title_full On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms
title_fullStr On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms
title_full_unstemmed On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms
title_sort on constructing constrained tree automata recognizing ground instances of constrained terms
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2013-11-01
description 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.
url http://arxiv.org/pdf/1311.5567v1
work_keys_str_mv AT naokinishida onconstructingconstrainedtreeautomatarecognizinggroundinstancesofconstrainedterms
AT masahikosakai onconstructingconstrainedtreeautomatarecognizinggroundinstancesofconstrainedterms
AT yasuhironakano onconstructingconstrainedtreeautomatarecognizinggroundinstancesofconstrainedterms
_version_ 1725586123656265728

Similar Items