MTT: The Maude Termination Tool (System Description)

DOI10.1007/978-3-540-71070-7_27zbMath1165.68360OpenAlexW2158673451MaRDI QIDQ3541712

Francisco Durán, Salvador Lucas, José Meseguer

Publication date: 27 November 2008

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_27

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theory of software (68N99)

Related Items (21)

Sentence-normalized conditional narrowing modulo in rewriting logic and Maude ⋮ Dependency pairs for proving termination properties of conditional term rewriting systems ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Two Decades of Maude ⋮ Twenty years of rewriting logic ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Sufficient completeness verification for conditional and constrained TRS ⋮ Optimizing Maude programs via program specialization ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Behavioral Rewrite Systems and Behavioral Productivity ⋮ Operational Termination of Membership Equational Programs: the Order-Sorted Way ⋮ A compact fixpoint semantics for term rewriting systems ⋮ Integrating Maude into Hets ⋮ Proving Termination Properties with mu-term ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Applications and extensions of context-sensitive rewriting ⋮ Methods for Proving Termination of Rewriting-based Programming Languages by Transformation ⋮ Termination Modulo Combinations of Equational Theories ⋮ Localized Operational Termination in General Logics ⋮ Symbolic computation in Maude: some tapas

Uses Software

• Maude
• MTT
• MU-TERM

Cites Work

• 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
• ELAN from a rewriting logic point of view
• Context-sensitive rewriting strategies
• Specification and proof in membership equational logic
• Proving operational termination of membership equational programs
• Semantic foundations for generalized rewrite theories
• Order-sorted termination: The unsorted way
• Operational Termination of Membership Equational Programs: the Order-Sorted Way
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: MTT: The Maude Termination Tool (System Description)