Termination of term rewriting using dependency pairs
From MaRDI portal
Publication:1978641
Recommendations
Cites work
- Automatic termination proofs with transformation orderings
- Automating the Knuth Bendix ordering
- Counterexamples to termination for the direct sum of term rewriting systems
- Dummy elimination: Making termination easier
- Generating polynomial orderings
- Generating polynomial orderings for termination proofs
- scientific article; zbMATH DE number 4047065 (Why is no real title available?)
- scientific article; zbMATH DE number 3688776 (Why is no real title available?)
- scientific article; zbMATH DE number 3729436 (Why is no real title available?)
- scientific article; zbMATH DE number 108434 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1142319 (Why is no real title available?)
- scientific article; zbMATH DE number 1761896 (Why is no real title available?)
- scientific article; zbMATH DE number 1380897 (Why is no real title available?)
- scientific article; zbMATH DE number 794237 (Why is no real title available?)
- scientific article; zbMATH DE number 794239 (Why is no real title available?)
- scientific article; zbMATH DE number 794240 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- Modular proofs for completeness of hierarchical term rewriting systems
- Natural termination
- On proving termination by innermost termination
- Orderings for term-rewriting systems
- Proving innermost normalisation automatically
- Proving termination of (conditional) rewrite systems. A semantic approach
- Pushing the frontiers of combining rewrite systems farther outwards
- Rewriting techniques and applications. 9th international conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998. Proceedings
- Simple termination of rewrite systems
- Termination by absence of infinite chains of dependency pairs
- Termination by completion
- Termination of constructor systems
- Termination of nested and mutually recursive algorithms
- Termination of rewriting
- Termination of rewriting systems by polynomial interpretations and its implementation
- Termination of term rewriting using dependency pairs
- Termination of term rewriting: Interpretation and type elimination
Cited in
(only showing first 100 items - show all)- Generating priority rewrite systems for OSOS process languages
- Termination of narrowing revisited
- Match-bounds revisited
- Increasing interpretations
- On normalizing, non-terminating one-rule string rewriting systems
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- Use of logical models for proving infeasibility in term rewriting
- Hierarchical termination revisited.
- Context-sensitive rewriting strategies
- Modular termination proofs for rewriting using dependency pairs
- Right-linear half-monadic term rewrite systems
- Total termination of term rewriting
- Jumping and escaping: modular termination and the abstract path ordering
- Determinization of conditional term rewriting systems
- Termination of term rewriting using dependency pairs
- Applications and extensions of context-sensitive rewriting
- Multi-dimensional interpretations for termination of term rewriting
- An automated approach to the Collatz conjecture
- Derivational complexity and context-sensitive Rewriting
- Tuple interpretations for termination of term rewriting
- Formalization of the computational theory of a Turing complete functional language model
- Term orderings for non-reachability of (conditional) rewriting
- Pattern eliminating transformations
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- Using well-founded relations for proving operational termination
- Real or natural number interpretation and their effect on complexity
- Analyzing innermost runtime complexity of term rewriting by dependency pairs
- Relative termination via dependency pairs
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- Automating the dependency pair method
- On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
- Termination orders for three-dimensional rewriting
- The size-change principle and dependency pairs for termination of term rewriting
- Modular and incremental automated termination proofs
- Operational semantics of resolution and productivity in Horn clause logic
- Modular and incremental proofs of AC-termination
- A combination framework for complexity
- scientific article; zbMATH DE number 1722701 (Why is no real title available?)
- Using context-sensitive rewriting for proving innermost termination of rewriting
- Lazy rewriting and context-sensitive rewriting
- Approximations for strategies and termination
- Outermost ground termination
- Termination criteria for DPO transformations with injective matches
- Improving the context-sensitive dependency graph
- Proving termination of context-sensitive rewriting with MU-TERM
- Innermost termination of rewrite systems by labeling
- Decidability of innermost termination and context-sensitive termination for semi-constructor term rewriting systems
- Static slicing of rewrite systems
- Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
- Compression of rewriting systems for termination analysis
- A Lambda-Free Higher-Order Recursive Path Order
- Dependency triples for improving termination analysis of logic programs with cut
- Proving termination properties with \textsc{mu-term}
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- Harnessing first order termination provers using higher order dependency pairs
- Certification of Termination Proofs Using CeTA
- Improving dependency pairs
- A Finite Representation of the Narrowing Space
- Reducing relative termination to dependency pair problems
- Linear integer arithmetic revisited
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Modular Termination of Basic Narrowing
- Effectively Checking the Finite Variant Property
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Maximal Termination
- Usable Rules for Context-Sensitive Rewrite Systems
- Arctic Termination ...Below Zero
- Root-Labeling
- Deciding Innermost Loops
- Normalization of Infinite Terms
- Uncurrying for termination and complexity
- Paramodulation with non-monotonic orderings and simplification
- Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
- The Computability Path Ordering: The End of a Quest
- Automated Implicit Computational Complexity Analysis (System Description)
- Automated Complexity Analysis Based on the Dependency Pair Method
- Certifying a Termination Criterion Based on Graphs, without Graphs
- Signature extensions preserve termination. An alternative proof via dependency pairs
- From Outermost Termination to Innermost Termination
- Dependency Pairs for Rewriting with Non-free Constructors
- Proving Termination by Bounded Increase
- All-Termination(T)
- Automatic Termination
- Proving Termination of Integer Term Rewriting
- Dependency Pairs and Polynomial Path Orders
- Well-Definedness of Streams by Termination
- Local Termination
- From Outermost to Context-Sensitive Rewriting
- Proving Infinitary Normalization
- Degrees of Undecidability in Term Rewriting
- Argument filterings and usable rules for simply typed dependency pairs
- scientific article; zbMATH DE number 3921958 (Why is no real title available?)
- Proving termination by dependency pairs and inductive theorem proving
- scientific article; zbMATH DE number 2043534 (Why is no real title available?)
- scientific article; zbMATH DE number 1765695 (Why is no real title available?)
- scientific article; zbMATH DE number 1765702 (Why is no real title available?)
- Size-based termination of higher-order rewriting
- Checking termination of bottom-up evaluation of logic programs with function symbols
- Using linear constraints for logic program termination analysis
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)
