Termination of term rewriting using dependency pairs

DOI10.1016/S0304-3975(99)00207-8zbMath0938.68051OpenAlexW2090855107MaRDI QIDQ1978641

Publication date: 4 June 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(99)00207-8

zbMATH Keywords

verification termination term rewriting automated theorem proving dependency pairs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (only showing first 100 items - show all)

Relative termination via dependency pairs ⋮ A combination framework for complexity ⋮ Right-linear half-monadic term rewrite systems ⋮ Relaxing monotonicity for innermost termination ⋮ On proving \(C_E\)-termination of rewriting by size-change termination ⋮ Operational semantics of resolution and productivity in Horn clause logic ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ A Finite Representation of the Narrowing Space ⋮ Reducing Relative Termination to Dependency Pair Problems ⋮ Linear Integer Arithmetic Revisited ⋮ KBO orientability ⋮ Verifying termination and reduction properties about higher-order logic programs ⋮ Termination of string rewriting proved automatically ⋮ Certification of Termination Proofs Using CeTA ⋮ Mechanically proving termination using polynomial interpretations ⋮ Modular and incremental proofs of AC-termination ⋮ Proving termination of context-sensitive rewriting by transformation ⋮ 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 ⋮ Paramodulation with non-monotonic orderings and simplification ⋮ Tyrolean termination tool: techniques and features ⋮ Elimination transformations for associative-commutative rewriting systems ⋮ Mechanizing and improving dependency pairs ⋮ An integrated framework for the diagnosis and correction of rule-based programs ⋮ Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting ⋮ Jumping and escaping: modular termination and the abstract path ordering ⋮ Determinization of conditional term rewriting systems ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Levels of undecidability in rewriting ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Modular Termination of Basic Narrowing ⋮ Effectively Checking the Finite Variant Property ⋮ Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures ⋮ Maximal Termination ⋮ Usable Rules for Context-Sensitive Rewrite Systems ⋮ Arctic Termination ...Below Zero ⋮ Root-Labeling ⋮ Deciding Innermost Loops ⋮ Normalization of Infinite Terms ⋮ Some classes of term rewriting systems inferable from positive data ⋮ A Lambda-Free Higher-Order Recursive Path Order ⋮ Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems ⋮ The Computability Path Ordering: The End of a Quest ⋮ Matrix interpretations for proving termination of term rewriting ⋮ Automated Implicit Computational Complexity Analysis (System Description) ⋮ 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 ⋮ Enhancing dependency pair method using strong computability in simply-typed term rewriting ⋮ Dependency Triples for Improving Termination Analysis of Logic Programs with Cut ⋮ Termination of term rewriting using dependency pairs ⋮ Loop detection in term rewriting using the eliminating unfoldings ⋮ Adding constants to string rewriting ⋮ Use of logical models for proving infeasibility in term rewriting ⋮ Unnamed Item ⋮ Termination of narrowing via termination of rewriting ⋮ Automating the dependency pair method ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ Characterizing and proving operational termination of deterministic conditional term rewriting systems ⋮ From Outermost Termination to Innermost Termination ⋮ On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting ⋮ Context-sensitive dependency pairs ⋮ Termination orders for three-dimensional rewriting ⋮ Normal forms and normal theories in conditional rewriting ⋮ Proving Termination Properties with mu-term ⋮ The Hydra battle and Cichon's principle ⋮ All-Termination(T) ⋮ Applications and extensions of context-sensitive rewriting ⋮ Using Context-Sensitive Rewriting for Proving Innermost Termination of Rewriting ⋮ Generating priority rewrite systems for OSOS process languages ⋮ Using well-founded relations for proving operational termination ⋮ Multi-dimensional interpretations for termination of term rewriting ⋮ An automated approach to the Collatz conjecture ⋮ Automatic Termination ⋮ 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 ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Termination of narrowing revisited ⋮ Lazy Rewriting and Context-Sensitive Rewriting ⋮ On normalizing, non-terminating one-rule string rewriting systems ⋮ Match-bounds revisited ⋮ Increasing interpretations ⋮ The size-change principle and dependency pairs for termination of term rewriting ⋮ Hierarchical termination revisited. ⋮ Context-sensitive rewriting strategies ⋮ Modular and incremental automated termination proofs ⋮ Tuple interpretations for termination of term rewriting ⋮ Formalization of the computational theory of a Turing complete functional language model ⋮ Term orderings for non-reachability of (conditional) rewriting ⋮ Improving the Context-sensitive Dependency Graph ⋮ Proving Termination of Context-Sensitive Rewriting with MU-TERM ⋮ Real or natural number interpretation and their effect on complexity ⋮ Modular termination proofs for rewriting using dependency pairs ⋮ Analyzing innermost runtime complexity of term rewriting by dependency pairs ⋮ Innermost Termination of Rewrite Systems by Labeling ⋮ Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems ⋮ Static Slicing of Rewrite Systems ⋮ Pattern eliminating transformations

Uses Software

REVE

Cites Work

This page was built for publication: Termination of term rewriting using dependency pairs