Termination of term rewriting using dependency pairs
From MaRDI portal
Publication:1978641
DOI10.1016/S0304-3975(99)00207-8zbMATH Open0938.68051OpenAlexW2090855107MaRDI QIDQ1978641FDOQ1978641
Authors: Yanyan Li 
Publication date: 4 June 2000
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0304-3975(99)00207-8
Recommendations
Cites Work
- Termination of rewriting systems by polynomial interpretations and its implementation
- Termination of term rewriting: Interpretation and type elimination
- Termination of term rewriting using dependency pairs
- Orderings for term-rewriting systems
- Title not available (Why is that?)
- Termination of rewriting
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Counterexamples to termination for the direct sum of term rewriting systems
- Proving innermost normalisation automatically
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Natural termination
- Automating the Knuth Bendix ordering
- Termination by completion
- Modular proofs for completeness of hierarchical term rewriting systems
- Proving termination of (conditional) rewrite systems. A semantic approach
- Rewriting techniques and applications. 9th international conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998. Proceedings
- Termination of nested and mutually recursive algorithms
- Generating polynomial orderings
- Generating polynomial orderings for termination proofs
- Simple termination of rewrite systems
- Title not available (Why is that?)
- Dummy elimination: Making termination easier
- On proving termination by innermost termination
- Termination by absence of infinite chains of dependency pairs
- Pushing the frontiers of combining rewrite systems farther outwards
- Automatic termination proofs with transformation orderings
- Termination of constructor systems
Cited In (only showing first 100 items - show all)
- Termination of Narrowing in Left-Linear Constructor Systems
- Towards a systematic method for proving termination of graph transformation systems
- Total termination of term rewriting
- Tuple interpretations for termination of term rewriting
- Analysing parallel complexity of term rewriting
- mu-term: Verify Termination Properties Automatically (System Description)
- Title not available (Why is that?)
- Automatic Termination
- The Computability Path Ordering: The End of a Quest
- Term orderings for non-reachability of (conditional) rewriting
- Pattern eliminating transformations
- Termination checking with types
- Using well-founded relations for proving operational termination
- Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
- Operational semantics of resolution and productivity in Horn clause logic
- Termination of narrowing revisited
- On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
- Proving termination of context-sensitive rewriting by transformation
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- Size-based termination of higher-order rewriting
- Use of logical models for proving infeasibility in term rewriting
- Right-linear half-monadic term rewrite systems
- Termination by absence of infinite chains of dependency pairs
- Applications and extensions of context-sensitive rewriting
- Checking termination of bottom-up evaluation of logic programs with function symbols
- Elimination transformations for associative-commutative rewriting systems
- Generating priority rewrite systems for OSOS process languages
- Termination of constructor systems
- Jumping and escaping: modular termination and the abstract path ordering
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- On proving termination by innermost termination
- Efficient Unfolding of Fuzzy Connectives for Multi-adjoint Logic Programs
- An automated approach to the Collatz conjecture
- An automated approach to the Collatz conjecture
- Modular and incremental automated termination proofs
- A Finite Representation of the Narrowing Space
- Proving Termination of Integer Term Rewriting
- Static slicing of rewrite systems
- Increasing interpretations
- Compression of rewriting systems for termination analysis
- Some classes of term rewriting systems inferable from positive data
- Using context-sensitive rewriting for proving innermost termination of rewriting
- A Lambda-Free Higher-Order Recursive Path Order
- The size-change principle and dependency pairs for termination of term rewriting
- Usable Rules for Context-Sensitive Rewrite Systems
- Modular and incremental proofs of AC-termination
- Approximations for strategies and termination
- Derivational complexity and context-sensitive Rewriting
- Proving Infinitary Normalization
- Loop detection in term rewriting using the eliminating unfoldings
- Adding constants to string rewriting
- Formalization of the computational theory of a Turing complete functional language model
- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
- Real or natural number interpretation and their effect on complexity
- Proving innermost normalisation automatically
- Match-bounds revisited
- Multi-dimensional interpretations for termination of term rewriting
- On proving \(C_E\)-termination of rewriting by size-change termination
- Relaxing monotonicity for innermost termination
- Certification of Proving Termination of Term Rewriting by Matrix Interpretations
- Increasing Interpretations
- Complexity of Fractran and Productivity
- A combination framework for complexity
- Effectively Checking the Finite Variant Property
- Uncurrying for termination and complexity
- Proving termination of context-sensitive rewriting with MU-TERM
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- Automating the dependency pair method
- Transforming termination by self-labelling
- Certification of Termination Proofs Using CeTA
- Termination of narrowing via termination of rewriting
- Normalization of Infinite Terms
- Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
- The Derivational Complexity Induced by the Dependency Pair Method
- Beyond Dependency Graphs
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- Degrees of Undecidability in Term Rewriting
- Automating the dependency pair method.
- Logic for Programming, Artificial Intelligence, and Reasoning
- Polynomials over the reals in proofs of termination : from theory to practice
- Linear integer arithmetic revisited
- Hierarchical termination revisited.
- Proving termination by dependency pairs and inductive theorem proving
- Determinization of conditional term rewriting systems
- Search Techniques for Rational Polynomial Orders
- Title not available (Why is that?)
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- On normalizing, non-terminating one-rule string rewriting systems
- KBO orientability
- Mechanically proving termination using polynomial interpretations
- Verifying termination and reduction properties about higher-order logic programs
- Termination of Narrowing Using Dependency Pairs
- An integrated framework for the diagnosis and correction of rule-based programs
- Improving dependency pairs
- A dependency pair framework for innermost complexity analysis of term rewrite systems
- Modular termination proofs for rewriting using dependency pairs
- Termination of term rewriting using dependency pairs
- Local Termination
Uses Software
This page was built for publication: Termination of term rewriting using dependency pairs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1978641)
