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

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