Termination of term rewriting using dependency pairs

DOI10.1016/S0304-3975(99)00207-8zbMATH Open0938.68051OpenAlexW2090855107MaRDI QIDQ1978641FDOQ1978641

Authors: Yanyan Li 

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

Recommendations

• Automated Reasoning
• Modular termination proofs for rewriting using dependency pairs
• Improving dependency pairs
• Mechanizing and improving dependency pairs

zbMATH Keywords

verificationterm rewritingautomated theorem provingterminationdependency pairs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites Work

• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination of term rewriting: Interpretation and type elimination
• Termination of term rewriting using dependency pairs
• Orderings for term-rewriting systems
• Title not available (Why is that?)
• Termination of rewriting
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Counterexamples to termination for the direct sum of term rewriting systems
• Proving innermost normalisation automatically
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Natural termination
• Automating the Knuth Bendix ordering
• Termination by completion
• Modular proofs for completeness of hierarchical term rewriting systems
• Proving termination of (conditional) rewrite systems. A semantic approach
• Rewriting techniques and applications. 9th international conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998. Proceedings
• Termination of nested and mutually recursive algorithms
• Generating polynomial orderings
• Generating polynomial orderings for termination proofs
• Simple termination of rewrite systems
• Title not available (Why is that?)
• Dummy elimination: Making termination easier
• On proving termination by innermost termination
• Termination by absence of infinite chains of dependency pairs
• Pushing the frontiers of combining rewrite systems farther outwards
• Automatic termination proofs with transformation orderings
• Termination of constructor systems

Cited In (only showing first 100 items - show all)

• Termination of Narrowing in Left-Linear Constructor Systems
• Towards a systematic method for proving termination of graph transformation systems
• Total termination of term rewriting
• Tuple interpretations for termination of term rewriting
• Analysing parallel complexity of term rewriting
• mu-term: Verify Termination Properties Automatically (System Description)
• Title not available (Why is that?)
• Automatic Termination
• The Computability Path Ordering: The End of a Quest
• Term orderings for non-reachability of (conditional) rewriting
• Pattern eliminating transformations
• Termination checking with types
• Using well-founded relations for proving operational termination
• Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems
• Operational semantics of resolution and productivity in Horn clause logic
• Termination of narrowing revisited
• On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
• Proving termination of context-sensitive rewriting by transformation
• The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
• Size-based termination of higher-order rewriting
• Use of logical models for proving infeasibility in term rewriting
• Right-linear half-monadic term rewrite systems
• Termination by absence of infinite chains of dependency pairs
• Applications and extensions of context-sensitive rewriting
• Checking termination of bottom-up evaluation of logic programs with function symbols
• Elimination transformations for associative-commutative rewriting systems
• Generating priority rewrite systems for OSOS process languages
• Termination of constructor systems
• Jumping and escaping: modular termination and the abstract path ordering
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
• On proving termination by innermost termination
• Efficient Unfolding of Fuzzy Connectives for Multi-adjoint Logic Programs
• An automated approach to the Collatz conjecture
• An automated approach to the Collatz conjecture
• Modular and incremental automated termination proofs
• A Finite Representation of the Narrowing Space
• Proving Termination of Integer Term Rewriting
• Static slicing of rewrite systems
• Increasing interpretations
• Compression of rewriting systems for termination analysis
• Some classes of term rewriting systems inferable from positive data
• Using context-sensitive rewriting for proving innermost termination of rewriting
• A Lambda-Free Higher-Order Recursive Path Order
• The size-change principle and dependency pairs for termination of term rewriting
• Usable Rules for Context-Sensitive Rewrite Systems
• Modular and incremental proofs of AC-termination
• Approximations for strategies and termination
• Derivational complexity and context-sensitive Rewriting
• Proving Infinitary Normalization
• Loop detection in term rewriting using the eliminating unfoldings
• Adding constants to string rewriting
• Formalization of the computational theory of a Turing complete functional language model
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• Real or natural number interpretation and their effect on complexity
• Title not available (Why is that?)
• All-Termination(T)
• Harnessing first order termination provers using higher order dependency pairs
• Reducing relative termination to dependency pair problems
• Dependency triples for improving termination analysis of logic programs with cut
• Argument filterings and usable rules for simply typed dependency pairs
• Transforming SAT into termination of rewriting
• Root-Labeling
• Certifying a Termination Criterion Based on Graphs, without Graphs
• Relative termination via dependency pairs
• Termination of dependently typed rewrite rules
• Logic programming with function symbols: checking termination of bottom-up evaluation through program adornments
• SAT solving for termination proofs with recursive path orders and dependency pairs
• Deciding Innermost Loops
• Modular Termination of Basic Narrowing
• Dependency Pairs for Rewriting with Non-free Constructors
• On complexity bounds and confluence of parallel term rewriting
• Automated Implicit Computational Complexity Analysis (System Description)
• Dependency Pairs and Polynomial Path Orders
• From innermost to full almost-sure termination of probabilistic term rewriting
• Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
• Weighted Path Orders Are Semantic Path Orders
• Using linear constraints for logic program termination analysis
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• Proving Termination with (Boolean) Satisfaction
• Termination Analysis of Logic Programs Based on Dependency Graphs
• Termination criteria for DPO transformations with injective matches
• Monotonicity criteria for polynomial interpretations over the naturals
• Decidability of innermost termination and context-sensitive termination for semi-constructor term rewriting systems
• Innermost termination of rewrite systems by labeling
• Proving innermost normalisation automatically
• Match-bounds revisited
• Multi-dimensional interpretations for termination of term rewriting
• On proving \(C_E\)-termination of rewriting by size-change termination
• Relaxing monotonicity for innermost termination
• Certification of Proving Termination of Term Rewriting by Matrix Interpretations
• Increasing Interpretations
• Complexity of Fractran and Productivity
• A combination framework for complexity
• Effectively Checking the Finite Variant Property
• Uncurrying for termination and complexity
• Proving termination of context-sensitive rewriting with MU-TERM
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Automating the dependency pair method
• Transforming termination by self-labelling

Uses Software

• REVE

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1978641)