Proving termination properties with \textsc{mu-term}

DOI10.1007/978-3-642-17796-5_12MaRDI QIDQ3067476zbMATH OpenOpenAlexFDO

Authors Beatriz Alarcón, Raúl Gutiérrez, 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)

Recommendations

• Proving termination of context-sensitive rewriting with MU-TERM
• Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs
• MTT: The Maude Termination Tool (System Description)
• scientific article; zbMATH DE number 3930339
• Using context-sensitive rewriting for proving innermost termination of rewriting

Cites work

• A dependency pair framework for \(A \vee C\)-termination
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Context-sensitive dependency pairs
• scientific article; zbMATH DE number 1332639 (Why is no real title available?)
• scientific article; zbMATH DE number 1948501 (Why is no real title available?)
• scientific article; zbMATH DE number 2090310 (Why is no real title available?)
• scientific article; zbMATH DE number 6027911 (Why is no real title available?)
• Loops under Strategies
• Mechanizing and improving dependency pairs
• MTT: The Maude Termination Tool (System Description)
• Polynomials over the reals in proofs of termination : from theory to practice
• Proving termination in the context-sensitive dependency pair framework
• Proving termination of context-sensitive rewriting by transformation
• Proving termination of context-sensitive rewriting with MU-TERM
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs
• Termination of rewriting with strategy annotations
• Termination of term rewriting using dependency pairs
• Transformation techniques for context-sensitive rewrite systems

Cited in

(16)

• 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
• 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
• Function Calls at Frozen Positions in Termination of Context-Sensitive Rewriting
• Constrained term rewriting tooL
• Dependency pairs for proving termination properties of conditional term rewriting systems
• MTT: The Maude Termination Tool (System Description)
• SAT modulo linear arithmetic for solving polynomial constraints
• mu-term: Verify Termination Properties Automatically (System Description)
• Nagoya termination tool
• AC completion with termination tools
• Localized operational termination in general logics
• Hydra battles and AC termination

Describes a project that uses

Uses Software

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

This page was built for publication: Proving termination properties with \textsc{mu-term}

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