Termination of non-simple rewrite systems
Explore this paper's citation graph
Summary
There are appendices describing the interface to code written in common lisp which implements the well-quasi general path ordering and showing its usage to prove termination of a rewrite system for insertion sort.
- Type
- article
- Published
- 1996-01-01
- Cited by
- 1
- References
- 87
- OpenAlex
- https://openalex.org/W42952197
- Semantic Scholar
- https://api.semanticscholar.org/CorpusID:115294457
Keywords
Rewriting, Simple (philosophy), Normalization property, Lexicographical order, Set (abstract data type)
References
- An Algorithm for Unification in Equational Theories
- On the Uniform Halting Problem for Term Rewriting Systems
- On the Halting of Tree Replacement Systems.
- Foundations of Software Technology and Theoretical Computer Science, 14th Conference, Madras, India, December 15-17, 1994, Proceedings
- Termination of Rewriting Systems by Polynomial Interpretations and Its Implementation
- Proving termination with multiset orderings
- Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s conjecture
- A Geometrical Approach to Multiset Orderings
- Orderings for term-rewriting systems
- An algorithm for finding canonical sets of ground rewrite rules in polynomial time
- Ordering by Divisibility in Abstract Algebras
- On Proving Uniform Termination and Restricted Termination of Rewriting Systems
- The Theory of Well-Quasi-Ordering: A Frequently Discovered Concept
- Common Lisp the Language
- Equational inference, canonical proofs, and proof orderings
- Computing in systems described by equations
- TERMINATION OF TERM REWRITING BY SEMANTIC LABELLING
- On Theories with a Combinatorial Definition of "Equivalence"
- Rewrite Systems
- Natural Termination