Mechanizing and improving dependency pairs

DOI10.1007/s10817-006-9057-7zbMath1113.68088OpenAlexW2001932052MaRDI QIDQ877836

René Thiemann, Jürgen Giesl, Peter Schneider-Kamp, Stephan Falke

Publication date: 3 May 2007

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-006-9057-7

zbMATH Keywords

AProVEautomated termination prover

Mathematics Subject Classification ID

Related Items (62)

Relative termination via dependency pairs ⋮ Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Unnamed Item ⋮ Automatically Proving and Disproving Feasibility Conditions ⋮ mu-term: Verify Termination Properties Automatically (System Description) ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Generalized and Formalized Uncurrying ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Reducing Relative Termination to Dependency Pair Problems ⋮ KBO orientability ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Uncurrying for termination and complexity ⋮ Mechanizing and improving dependency pairs ⋮ Size-based termination of higher-order rewriting ⋮ Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ 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 ⋮ Fast offline partial evaluation of logic programs ⋮ Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems ⋮ Automated Complexity Analysis Based on the Dependency Pair Method ⋮ Certifying a Termination Criterion Based on Graphs, without Graphs ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Dependency Triples for Improving Termination Analysis of Logic Programs with Cut ⋮ Termination of narrowing via termination of rewriting ⋮ An automated approach to the Collatz conjecture ⋮ Characterizing and proving operational termination of deterministic conditional term rewriting systems ⋮ From Outermost Termination to Innermost Termination ⋮ Termination Analysis by Dependency Pairs and Inductive Theorem Proving ⋮ Beyond Dependency Graphs ⋮ Unnamed Item ⋮ Context-sensitive dependency pairs ⋮ A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems ⋮ Proving Termination Properties with mu-term ⋮ Termination of Narrowing in Left-Linear Constructor Systems ⋮ Applications and extensions of context-sensitive rewriting ⋮ Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting ⋮ Using well-founded relations for proving operational termination ⋮ Multi-dimensional interpretations for termination of term rewriting ⋮ An automated approach to the Collatz conjecture ⋮ Automatic generation of logical models with AGES ⋮ Proving Termination of Integer Term Rewriting ⋮ Proving Confluence of Term Rewriting Systems Automatically ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Argument Filterings and Usable Rules for Simply Typed Dependency Pairs ⋮ Match-bounds revisited ⋮ Increasing interpretations ⋮ Termination Analysis of Logic Programs Based on Dependency Graphs ⋮ Termination of Narrowing Using Dependency Pairs ⋮ Search Techniques for Rational Polynomial Orders ⋮ Increasing Interpretations ⋮ Localized Operational Termination in General Logics ⋮ Tuple interpretations for termination of term rewriting ⋮ Term orderings for non-reachability of (conditional) rewriting ⋮ Analyzing innermost runtime complexity of term rewriting by dependency pairs ⋮ Innermost Termination of Rewrite Systems by Labeling ⋮ Pattern eliminating transformations

Uses Software

• TALP
• Haskell
• Tyrolean
• AProVE
• TPA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
• Proofs by induction in equational theories with constructors
• Termination of string rewriting proved automatically
• Mechanizing and improving dependency pairs
• Termination of rewriting
• Counterexamples to termination for the direct sum of term rewriting systems
• Testing positiveness of polynomials
• Generalized sufficient conditions for modular termination of rewriting
• Match-bounded string rewriting systems
• Modular termination proofs for rewriting using dependency pairs
• Termination of term rewriting using dependency pairs
• Automating the dependency pair method
• The size-change principle and dependency pairs for termination of term rewriting
• Modular and incremental automated termination proofs
• TPA: Termination Proved Automatically
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• Automated Termination Analysis for Logic Programs by Term Rewriting
• Term Rewriting and All That
• The size-change principle for program termination
• Automated Reasoning
• Polynomials over the reals in proofs of termination : from theory to practice
• Artificial Intelligence and Symbolic Computation
• Frontiers of Combining Systems
• Term Rewriting and Applications
• Logic for Programming, Artificial Intelligence, and Reasoning
• Rewriting Techniques and Applications
• Verification of Erlang processes by dependency pairs
• A general framework for automatic termination analysis od logic programs

This page was built for publication: Mechanizing and improving dependency pairs