Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
From MaRDI portal
Publication:673975
DOI10.1016/0304-3975(94)00135-6zbMATH Open0874.68156OpenAlexW2049865932MaRDI QIDQ673975FDOQ673975
Authors: Andreas Weiermann 
Publication date: 28 February 1997
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(94)00135-6
Recommendations
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Uniform Approach to Fundamental Sequences and Hierarchies
- Termination proofs by multiset path orderings imply primitive recursive derivation lengths
- Title not available (Why is that?)
- Eine Klassifikation der ε0‐Rekursiven Funktionen
- Bounding derivation lengths with functions from the slow growing hierarchy
- Title not available (Why is that?)
- Slow growing versus fast growing
- Incremental termination proofs and the length of derivations
Cited In (35)
- A lexicographic path order with slow growing derivation bounds
- Termination proofs and the length of derivations
- Termination proofs by multiset path orderings imply primitive recursive derivation lengths
- Bounding derivation lengths with functions from the slow growing hierarchy
- Proving consistency of equational theories in bounded arithmetic
- Quasi-interpretations. A way to control resources
- An upper bound on the derivational complexity of Knuth-Bendix orderings.
- Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones
- The Derivational Complexity Induced by the Dependency Pair Method
- Title not available (Why is that?)
- Complexity Analysis by Rewriting
- How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study
- Rewriting Techniques and Applications
- KBO orientability
- Applications and extensions of context-sensitive rewriting
- Analytic combinatorics, proof-theoretic ordinals, and phase transitions for independence results
- The hierarchy of terminating recursive programs over N
- Proving Quadratic Derivational Complexities Using Context Dependent Interpretations
- Termination proofs by multiset path orderings imply primitive recursive derivation lengths
- Some interesting connections between the slow growing hierarchy and the Ackermann function
- Formalizing termination proofs under polynomial quasi-interpretations
- Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
- On the Computational Content of Termination Proofs
- The Hydra battle and Cichon's principle
- Derivation lengths and order types of Knuth--Bendix orders
- Strictly orthogonal left linear rewrite systems and primitive recursion
- Predicative lexicographic path orders. An application of term rewriting to the region of primitive recursive functions
- Title not available (Why is that?)
- Automated Complexity Analysis Based on the Dependency Pair Method
- Proof-theoretic analysis of termination proofs
- Incremental termination proofs and the length of derivations
- Derivational complexity and context-sensitive Rewriting
- Some results on cut-elimination, provable well-orderings, induction and reflection
- Analyzing Innermost Runtime Complexity Through Tuple Interpretations
- Term rewriting theory for the primitive recursive functions
This page was built for publication: Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q673975)
