Dependency pairs for proving termination properties of conditional term rewriting systems
From MaRDI portal
Publication:347382
DOI10.1016/j.jlamp.2016.03.003zbMath1353.68155OpenAlexW2333572417MaRDI QIDQ347382
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
Related Items
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
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
