The dependency pair framework: Combining techniques for automated termination proofs
From MaRDI portal
Recommendations
Cited in
(72)- Match-bounds revisited
- Increasing interpretations
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- Multi-dimensional interpretations for termination of term rewriting
- Tuple interpretations for termination of term rewriting
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- Using well-founded relations for proving operational termination
- Analyzing innermost runtime complexity of term rewriting by 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
- The size-change principle and dependency pairs for termination of term rewriting
- Proving termination of context-sensitive rewriting with MU-TERM
- Dependency triples for improving termination analysis of logic programs with cut
- Certification of Termination Proofs Using CeTA
- Improving dependency pairs
- Encoding dependency pair techniques and control strategies for maximal completion
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Maximal Termination
- Usable Rules for Context-Sensitive Rewrite Systems
- Root-Labeling
- Deciding Innermost Loops
- Uncurrying for termination and complexity
- Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
- The Computability Path Ordering: The End of a Quest
- The dependency triple framework for termination of logic programs
- From Outermost Termination to Innermost Termination
- Proving Termination of Integer Term Rewriting
- Well-Definedness of Streams by Termination
- Degrees of Undecidability in Term Rewriting
- Real_Impl
- Proving termination by dependency pairs and inductive theorem proving
- A dependency pair framework for \(A \vee C\)-termination
- Transforming SAT into termination of rewriting
- Dependency pairs termination in dependent type theory modulo rewriting
- Completion after program inversion of injective functions
- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- Beyond Dependency Graphs
- A dependency pair framework for innermost complexity analysis of term rewrite systems
- On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
- Structural rewriting in the pi-calculus
- Automated Reasoning
- Termination proofs in the dependency pair framework May induce multiple recursive derivational complexity
- Certification of Proving Termination of Term Rewriting by Matrix Interpretations
- Frontiers of Combining Systems
- Termination Analysis of Logic Programs Based on Dependency Graphs
- Termination of Narrowing Using Dependency Pairs
- Search Techniques for Rational Polynomial Orders
- Monotonicity criteria for polynomial interpretations over the naturals
- A static higher-order dependency pair framework
- Levels of undecidability in rewriting
- Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
- Proving confluence in the confluence framework with confident
- On basic feasible functionals and the interpretation method
- Wanda -- a higher-order termination tool (system description)
- Certifying the weighted path order (invited talk)
- A characterization of basic feasible functionals through higher-order rewriting and tuple interpretations
- Lexicographic combination of reduction pairs
- Termination of generalized term rewriting systems
- Simulating dependency pairs by semantic labeling
- A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems
- A dependency pair framework for relative termination of term rewriting
- Higher-order constrained dependency pairs for (universal) computability
- KBO orientability
- Proving termination of context-sensitive rewriting by transformation
- Mechanizing and improving dependency pairs
- Matrix interpretations for proving termination of term rewriting
- Loop detection in term rewriting using the eliminating unfoldings
- Adding constants to string rewriting
- Termination of narrowing via termination of rewriting
- Context-sensitive dependency pairs
This page was built for publication: The dependency pair framework: Combining techniques for automated termination proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5705932)
