The theory of ground rewrite systems is decidable
- 4 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 242-248
- https://doi.org/10.1109/lics.1990.113750
Abstract
Using tree automata techniques, it is proven that the theory of ground rewrite systems is decidable. Novel decision procedures are presented for most classic properties of ground rewrite systems. An example is presented to illustrate how these results could be used for specification and debugging.Keywords
This publication has 15 references indexed in Scilit:
- Decidability of confluence for ground term rewriting systemsPublished by Springer Nature ,2006
- Theorem proving using equational matings and rigid E -unificationJournal of the ACM, 1992
- Termination of rewritingJournal of Symbolic Computation, 1987
- Editorial boardJournal of Symbolic Computation, 1987
- Equivalences and transformations of regular systems—Applications to recursive program schemes and grammarsTheoretical Computer Science, 1986
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- Bottom-up and top-down tree transformations— a comparisonTheory of Computing Systems, 1975
- Generalized finite automata theory with an application to a decision problem of second-order logicTheory of Computing Systems, 1968
- Automata in general algebrasInformation and Control, 1967
- Algebraic automata and context-free setsInformation and Control, 1967