Back to Search
Start Over
On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms
- Source :
- Electronic Proceedings in Theoretical Computer Science, Vol 134, Iss Proc. TTATT 2013, Pp 1-10 (2013)
- Publication Year :
- 2013
- Publisher :
- Open Publishing Association, 2013.
-
Abstract
- 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.
- Subjects :
- Mathematics
QA1-939
Electronic computers. Computer science
QA75.5-76.95
Subjects
Details
- Language :
- English
- ISSN :
- 20752180 and 86584316
- Volume :
- 134
- Issue :
- Proc. TTATT 2013
- Database :
- Directory of Open Access Journals
- Journal :
- Electronic Proceedings in Theoretical Computer Science
- Publication Type :
- Academic Journal
- Accession number :
- edsdoj.25fa60ed8658431688b19cde85019fd6
- Document Type :
- article
- Full Text :
- https://doi.org/10.4204/EPTCS.134.1