mu-term: Verify Termination Properties Automatically (System Description)
From MaRDI portal
Publication:5049021
DOI10.1007/978-3-030-51054-1_28OpenAlexW3038988094MaRDI QIDQ5049021
Salvador Lucas, Raúl Gutiérrez
Publication date: 9 November 2022
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-51054-1_28
Related Items (4)
Applications and extensions of context-sensitive rewriting ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Tuple interpretations for termination of term rewriting ⋮ Term orderings for non-reachability of (conditional) rewriting
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Dependency pairs for proving termination properties of conditional term rewriting systems
- Mechanizing and improving dependency pairs
- Matrix interpretations for proving termination of term rewriting
- 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
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Termination of term rewriting: Interpretation and type elimination
- 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
- Use of logical models for proving infeasibility in term rewriting
- Context-sensitive rewriting strategies
- Termination of term rewriting using dependency pairs
- Proving semantic properties as first-order satisfiability
- Automatic generation of logical models with AGES
- Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
- Order-sorted termination: The unsorted way
- Proving Termination Properties with mu-term
- Termination of context-sensitive rewriting
- Proving Termination in the Context-Sensitive Dependency Pair Framework
- A Dependency Pair Framework for A ∨ C-Termination
- Automatically Proving and Disproving Feasibility Conditions
- Frontiers of Combining Systems
- Improving Context-Sensitive Dependency Pairs
- Verification of Erlang processes by dependency pairs
This page was built for publication: mu-term: Verify Termination Properties Automatically (System Description)
