Dependency pairs for proving termination properties of conditional term rewriting systems

DOI10.1016/j.jlamp.2016.03.003zbMath1353.68155OpenAlexW2333572417MaRDI QIDQ347382

José Meseguer, Salvador Lucas

Publication date: 30 November 2016

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2016.03.003

zbMATH Keywords

program analysisconditional term rewritingdependency pairsoperational termination

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (9)

mu-term: Verify Termination Properties Automatically (System Description) ⋮ The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Use of logical models for proving infeasibility in term rewriting ⋮ Applications and extensions of context-sensitive rewriting ⋮ Using well-founded relations for proving operational termination ⋮ Automatic generation of logical models with AGES ⋮ Term orderings for non-reachability of (conditional) rewriting

Uses Software

• ELAN
• Haskell
• OBJ3
• CafeOBJ
• Maude
• Tyrolean
• AProVE
• MTT
• VMTL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Characterizing and proving operational termination of deterministic conditional term rewriting systems
• Normal forms and normal theories in conditional rewriting
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• A rationale for conditional equational programming
• Context-sensitive dependency pairs
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Operational termination of conditional term rewriting systems
• Conditional rewrite rules
• Conditional rewrite rules: Confluence and termination
• IThe 2nd international workshop on rewriting logic and its applications, RWLW.. Abbaye des Prèmontrès at Pont-á-Mousson, France, September 1998
• Termination of term rewriting using dependency pairs
• Proving operational termination of membership equational programs
• Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity
• 2D Dependency Pairs for Proving Operational Termination of CTRSs
• Extending the 2D Dependency Pair Framework for Conditional Term Rewriting Systems
• Unravelings and ultra-properties
• Proving Termination Properties with mu-term
• Computationally Equivalent Elimination of Conditions
• MTT: The Maude Termination Tool (System Description)
• Signature Extensions Preserve Termination
• A Dependency Pair Framework for A ∨ C-Termination
• Logic Programming
• Logic for Programming, Artificial Intelligence, and Reasoning
• Rewriting Techniques and Applications

This page was built for publication: Dependency pairs for proving termination properties of conditional term rewriting systems