Termination Modulo Combinations of Equational Theories

DOI10.1007/978-3-642-04222-5_15zbMath1193.68145OpenAlexW1553416476MaRDI QIDQ3655204

Francisco Durán, José Meseguer, Salvador Lucas

Publication date: 7 January 2010

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2142/12311

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (13)

Order-sorted equational generalization algorithm revisited ⋮ Metalevel algorithms for variant satisfiability ⋮ Twenty years of rewriting logic ⋮ On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Normal forms and normal theories in conditional rewriting ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 ⋮ Termination Modulo Combinations of Equational Theories ⋮ Symbolic computation in Maude: some tapas

Uses Software

• Maude
• AProVE
• MTT
• REVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination of rewriting systems by polynomial interpretations and its implementation
• A total AC-compatible ordering based on RPO
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Combining matching algorithms: The regular case
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Termination and completion modulo associativity, commutativity and identity
• Completion for rewriting modulo a congruence
• Equational rules for rewriting logic
• Proving operational termination of membership equational programs
• Effectively Checking the Finite Variant Property
• MTT: The Maude Termination Tool (System Description)
• Termination Modulo Combinations of Equational Theories
• Completion of a Set of Rules Modulo a Set of Equations
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Complete Sets of Reductions for Some Equational Theories
• Variant Narrowing and Equational Unification
• Operational Termination of Membership Equational Programs: the Order-Sorted Way
• Term Rewriting and Applications

This page was built for publication: Termination Modulo Combinations of Equational Theories