Modular termination proofs for rewriting using dependency pairs
From MaRDI portal
Publication:1864874
DOI10.1006/jsco.2002.0541zbMath1010.68073OpenAlexW2030433877MaRDI QIDQ1864874
Jürgen Gieslthomas Artsenno Ohlebusch
Publication date: 23 March 2003
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/jsco.2002.0541
Related Items
A combination framework for complexity, Relaxing monotonicity for innermost termination, Transforming orthogonal inductive definition sets into confluent term rewrite systems, Knuth-Bendix completion of theories of commuting group endomorphisms, Verifying termination and reduction properties about higher-order logic programs, Mechanically proving termination using polynomial interpretations, Modular and incremental proofs of AC-termination, Proving termination of context-sensitive rewriting by transformation, Polynomials over the reals in proofs of termination : from theory to practice, Tyrolean termination tool: techniques and features, Elimination transformations for associative-commutative rewriting systems, Mechanizing and improving dependency pairs, Size-based termination of higher-order rewriting, Usable Rules for Context-Sensitive Rewrite Systems, Arctic Termination ...Below Zero, Automated Complexity Analysis Based on the Dependency Pair Method, Enhancing dependency pair method using strong computability in simply-typed term rewriting, Automating the dependency pair method, Proving operational termination of membership equational programs, Context-sensitive dependency pairs, Unnamed Item, TERMINATION OF ABSTRACT REDUCTION SYSTEMS, Proving Termination of Integer Term Rewriting, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Termination Analysis of Logic Programs Based on Dependency Graphs, The size-change principle and dependency pairs for termination of term rewriting, Hierarchical termination revisited.
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Natural termination
- Automating the Knuth Bendix ordering
- Termination of rewriting
- Counterexamples to termination for the direct sum of term rewriting systems
- On termination of the direct sum of term-rewriting systems
- A note on simplification orderings
- Modularity of simple termination of term rewriting systems with shared constructors
- Generating polynomial orderings
- Generalized sufficient conditions for modular termination of rewriting
- Termination of term rewriting: Interpretation and type elimination
- On the modularity of termination of term rewriting systems
- Modular proofs for completeness of hierarchical term rewriting systems
- Rewriting techniques and applications. 9th international conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998. Proceedings
- Simple termination of rewrite systems
- Rewriting techniques and applications. 11th international conference, RTA 2000, Norwich, GB, July 10--12, 2000. Proceedings
- Type introduction for equational rewriting
- Principles and practice of declarative programming. International conference PPDP '99. Paris, France, September 29--October 1, 1999. Proceedings
- Modular properties of composable term rewriting systems
- Termination of term rewriting using dependency pairs
- Completeness of combinations of constructor systems
- Termination for direct sums of left-linear complete term rewriting systems
- Generating polynomial orderings for termination proofs
- On proving termination by innermost termination
- Verification of Erlang processes by dependency pairs
- Termination of logic programs: Transformational methods revisited
