Mechanizing and improving dependency pairs
From MaRDI portal
Publication:877836
DOI10.1007/S10817-006-9057-7zbMATH Open1113.68088OpenAlexW2001932052MaRDI QIDQ877836FDOQ877836
Authors: Jürgen Giesl, René Thiemann, 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
Recommendations
- Improving dependency pairs
- Improving Context-Sensitive Dependency Pairs
- Automating the dependency pair method
- Rewriting Techniques and Applications
- Automating the dependency pair method.
- Improving the context-sensitive dependency graph
- Context-sensitive dependency pairs
- Context-Sensitive Dependency Pairs
- A static higher-order dependency pair framework
Cites Work
- Title not available (Why is that?)
- TPA: Termination Proved Automatically
- Modular termination proofs for rewriting using dependency pairs
- Termination of term rewriting using dependency pairs
- The size-change principle for program termination
- Rewriting Techniques and Applications
- Term Rewriting and All That
- Title not available (Why is that?)
- Termination of rewriting
- Title not available (Why is that?)
- Automating the dependency pair method
- Title not available (Why is that?)
- Title not available (Why is that?)
- Frontiers of Combining Systems
- Logic for Programming, Artificial Intelligence, and Reasoning
- Mechanizing and improving dependency pairs
- Proofs by induction in equational theories with constructors
- Counterexamples to termination for the direct sum of term rewriting systems
- Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
- Automated Termination Analysis for Logic Programs by Term Rewriting
- Polynomials over the reals in proofs of termination : from theory to practice
- On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
- Testing positiveness of polynomials
- Artificial Intelligence and Symbolic Computation
- Term Rewriting and Applications
- Improving dependency pairs
- Title not available (Why is that?)
- Verification of Erlang processes by dependency pairs
- Generalized sufficient conditions for modular termination of rewriting
- Title not available (Why is that?)
- Match-bounded string rewriting systems
- Termination of string rewriting proved automatically
- Automated Reasoning
- Modular and incremental automated termination proofs
- Title not available (Why is that?)
- A general framework for automatic termination analysis od logic programs
- The size-change principle and dependency pairs for termination of term rewriting
- Approximations for strategies and termination
Cited In (72)
- Title not available (Why is that?)
- Argument filterings and usable rules for simply typed dependency pairs
- Deciding Innermost Loops
- Proving confluence in the confluence framework with confident
- From innermost to full almost-sure termination of probabilistic term rewriting
- Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
- Termination of Narrowing in Left-Linear Constructor Systems
- Fast offline partial evaluation of logic programs
- Match-bounds revisited
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Tuple interpretations for termination of term rewriting
- Multi-dimensional interpretations for termination of term rewriting
- Automatic generation of logical models with AGES
- Automatically Proving and Disproving Feasibility Conditions
- mu-term: Verify Termination Properties Automatically (System Description)
- Increasing Interpretations
- Context-Sensitive Dependency Pairs
- 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
- Automating the dependency pair method
- Using well-founded relations for proving operational termination
- Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
- Termination of narrowing via termination of rewriting
- Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
- Reducing relative termination to dependency pair problems
- Beyond Dependency Graphs
- Termination Analysis by Dependency Pairs and Inductive Theorem Proving
- Frontiers of Combining Systems
- Automating the dependency pair method.
- Logic for Programming, Artificial Intelligence, and Reasoning
- 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
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- Size-based termination of higher-order rewriting
- Root-Labeling
- Certifying a Termination Criterion Based on Graphs, without Graphs
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Relative termination via dependency pairs
- KBO orientability
- Termination of Narrowing Using Dependency Pairs
- Applications and extensions of context-sensitive rewriting
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Improving dependency pairs
- A dependency pair framework for innermost complexity analysis of term rewrite systems
- Reachability analysis of innermost rewriting
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- Analyzing innermost runtime complexity of term rewriting by dependency pairs
- Localized operational termination in general logics
- An automated approach to the Collatz conjecture
- An automated approach to the Collatz conjecture
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Proving Termination of Integer Term Rewriting
- Increasing interpretations
- Using context-sensitive rewriting for proving innermost termination of rewriting
- Maximal Termination
- Characterizing and proving operational termination of deterministic conditional term rewriting systems
- Mechanizing and improving dependency pairs
- Usable Rules for Context-Sensitive Rewrite Systems
- Automated Complexity Analysis Based on the Dependency Pair Method
- Rewriting Techniques and Applications
- Context-sensitive dependency pairs
- Termination Analysis of Logic Programs Based on Dependency Graphs
- From Outermost Termination to Innermost Termination
- Derivational complexity and context-sensitive Rewriting
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- Innermost termination of rewrite systems by labeling
- Proving Confluence of Term Rewriting Systems Automatically
- Proving termination properties with \textsc{mu-term}
- Generalized and formalized uncurrying
Uses Software
This page was built for publication: Mechanizing and improving dependency pairs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q877836)
