Termination, AC-Termination and Dependency Pairs of Term Rewriting Systems
Explore this paper's citation graph
Summary
This thesis extends the notion of dependency pairs to AC-TRSs, and introduces new methods for effectively proving AC-termination, and proposes a new elimination transformation, called the argument filtering transformation, which is not only more powerful than all the other elimination transformations but also especially useful to make clear an essential relationship among them.
- Type
- article
- Published
- 2000-01-01
- Cited by
- 13
- References
- 71
- OpenAlex
- https://openalex.org/W7480855
- Semantic Scholar
- https://api.semanticscholar.org/CorpusID:16925786
Keywords
Rewriting, Term (time), Dependency (UML), Confluence, Computer science
References
- Computations in Orthogonal Rewriting Systems, II
- The hierarchy of dependency pairs
- On the Uniform Halting Problem for Term Rewriting Systems
- On proving AC-termination by argument filtering method
- Termination of term rewriting : well-foundedness, totality and transformations
- Computability and λ-definability
- On Proving AC-Termination by AC-Dependency Paris
- Reduction strategies for term rewriting systems
- On undecidable propositions of formal mathematical systems
- Term rewriting and all that
- Index Reduction of Overlapping Strongly Sequential Systems
- λ-definability and recursiveness
- Associative-Commutative Reduction Orderings
- A Total AC-Compatible Ordering Based on RPO
- A Note on Simplification Orderings
- Modularity of Simple Termination of Term Rewriting Systems with Shared Constructors
- Proving termination with multiset orderings
- Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s conjecture
- General recursive functions of natural numbers
- Simulation of Turing Machines by a Regular Rewrite Rule
Cited by
- Towards a Framework for Proving Termination of Maude Programs
- Approximations for Strategies and Termination
- AN OVERVIEW OF THE APPLICATIONS OF MULTISETS 1
- The Weighted Path Order for Termination of Term Rewriting
- AC-KBO revisited* †
- Termination of associative-commutative rewriting using dependency pairs criteria
- Approximating Dependency Graphs Using Tree Automata Techniques
- AN OVERVIEW OF THE APPLICATIONS OF MULTISETS
- AC Completion with Termination Tools
- AC-KBO Revisited
- A Dependency Pair Framework for A OR C-Termination
- Beyond Dependency Graphs
Related papers
- Termination of term rewriting using dependency pairs
- Term rewriting and all that
- On Proving AC-Termination by AC-Dependency Paris
- Decidability of Termination Properties for Term Rewriting Systems Consisting of Shallow Dependency Pairs
- Orderings for term-rewriting systems
- On Proving Termination of Term Rewriting Systems with Higher - Order Variables
- Modular and incremental proofs of AC-termination