Proving Termination Properties with mu-term

DOI10.1007/978-3-642-17796-5_12zbMath1308.68068OpenAlexW1677884663MaRDI QIDQ3067476

Raúl Gutiérrez, Beatriz Alarcón, Salvador Lucas, Rafael Navarro-Marset

Publication date: 21 January 2011

Published in: Algebraic Methodology and Software Technology (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-17796-5_12

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (12)

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 ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting ⋮ SAT modulo linear arithmetic for solving polynomial constraints ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ AC Completion with Termination Tools ⋮ Using well-founded relations for proving operational termination ⋮ Automatic generation of logical models with AGES ⋮ Use of Logical Models for Proving Operational Termination in General Logics ⋮ Localized Operational Termination in General Logics

Uses Software

• Maude
• AProVE
• MTT
• MU-TERM
• VMTL
• Jambox

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proving termination of context-sensitive rewriting by transformation
• Mechanizing and improving dependency pairs
• 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.
• Termination of term rewriting using dependency pairs
• Proving Termination of Context-Sensitive Rewriting with MU-TERM
• Termination of Rewriting with Strategy Annotations
• Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs
• MTT: The Maude Termination Tool (System Description)
• Loops under Strategies
• Proving Termination in the Context-Sensitive Dependency Pair Framework
• A Dependency Pair Framework for A ∨ C-Termination
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Polynomials over the reals in proofs of termination : from theory to practice
• Transformation techniques for context-sensitive rewrite systems

This page was built for publication: Proving Termination Properties with mu-term