Automating the dependency pair method

DOI10.1016/j.ic.2004.10.004zbMath1081.68038OpenAlexW2168096396MaRDI QIDQ2486583

Aart Middeldorp, Nao Hirokawa

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

zbMATH Keywords

TerminationTerm rewritingDependency pair method

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (32)

Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ KBO orientability ⋮ Certification of Termination Proofs Using CeTA ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Uncurrying for termination and complexity ⋮ 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 ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Maximal Termination ⋮ Root-Labeling ⋮ Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems ⋮ Matrix interpretations for proving termination of term rewriting ⋮ Dependency Triples for Improving Termination Analysis of Logic Programs with Cut ⋮ Monotonicity Criteria for Polynomial Interpretations over the Naturals ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Beyond Dependency Graphs ⋮ Context-sensitive dependency pairs ⋮ A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems ⋮ Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting ⋮ 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 ⋮ The Derivational Complexity Induced by the Dependency Pair Method ⋮ Match-bounds revisited ⋮ Increasing interpretations ⋮ Termination Analysis of Logic Programs Based on Dependency Graphs ⋮ Search Techniques for Rational Polynomial Orders ⋮ Increasing Interpretations ⋮ Term orderings for non-reachability of (conditional) rewriting ⋮ Analyzing innermost runtime complexity of term rewriting by dependency pairs ⋮ Pattern eliminating transformations

Uses Software

• Tsukuba

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination by completion
• Counterexamples to termination for the direct sum of term rewriting systems
• Hierarchical termination revisited.
• Context-sensitive rewriting strategies
• Modular termination proofs for rewriting using dependency pairs
• Termination of term rewriting using dependency pairs
• Modular and incremental proofs of AC-termination
• Automatic termination proofs with transformation orderings
• Automated Reasoning
• Artificial Intelligence and Symbolic Computation
• Transformation techniques for context-sensitive rewrite systems
• Rewriting Techniques and Applications
• Verification of Erlang processes by dependency pairs

This page was built for publication: Automating the dependency pair method