Automating the dependency pair method
From MaRDI portal
Publication:2486583
DOI10.1016/J.IC.2004.10.004zbMATH Open1081.68038OpenAlexW2168096396MaRDI QIDQ2486583FDOQ2486583
Authors: Nao Hirokawa, Aart Middeldorp 
Publication date: 5 August 2005
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2004.10.004
Recommendations
Cites Work
- Modular termination proofs for rewriting using dependency pairs
- Termination of term rewriting using dependency pairs
- Rewriting Techniques and Applications
- Title not available (Why is that?)
- Counterexamples to termination for the direct sum of term rewriting systems
- Context-sensitive rewriting strategies
- Artificial Intelligence and Symbolic Computation
- Improving dependency pairs
- Verification of Erlang processes by dependency pairs
- Title not available (Why is that?)
- Termination by completion
- Hierarchical termination revisited.
- Automated Reasoning
- Transformation techniques for context-sensitive rewrite systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Modular and incremental proofs of AC-termination
- Approximations for strategies and termination
- Automatic termination proofs with transformation orderings
- Title not available (Why is that?)
Cited In (35)
- Match-bounds revisited
- Increasing Interpretations
- Harnessing first order termination provers using higher order dependency pairs
- Term orderings for non-reachability of (conditional) rewriting
- Uncurrying for termination and complexity
- Pattern eliminating transformations
- Certification of Termination Proofs Using CeTA
- Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
- The Derivational Complexity Induced by the Dependency Pair Method
- Beyond Dependency Graphs
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- Automating the dependency pair method.
- Dependency triples for improving termination analysis of logic programs with cut
- Proving termination by dependency pairs and inductive theorem proving
- Search Techniques for Rational Polynomial Orders
- Size-based termination of higher-order rewriting
- Root-Labeling
- Automatic generation of make dependencies
- KBO orientability
- Elimination transformations for associative-commutative rewriting systems
- SAT solving for termination proofs with recursive path orders and dependency pairs
- A dependency pair framework for innermost complexity analysis of term rewrite systems
- Analyzing innermost runtime complexity of term rewriting by dependency pairs
- Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
- Proving Termination of Integer Term Rewriting
- Increasing interpretations
- Using context-sensitive rewriting for proving innermost termination of rewriting
- Maximal Termination
- Mechanizing and improving dependency pairs
- Tyrolean termination tool: techniques and features
- Matrix interpretations for proving termination of term rewriting
- Context-sensitive dependency pairs
- Termination Analysis of Logic Programs Based on Dependency Graphs
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- Monotonicity criteria for polynomial interpretations over the naturals
Uses Software
This page was built for publication: Automating the dependency pair method
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2486583)
