Ground confluence of order-sorted conditional specifications modulo axioms

DOI10.1016/j.jlamp.2019.100513zbMath1498.68073OpenAlexW2989726691WikidataQ126663663 ScholiaQ126663663MaRDI QIDQ2291829

Francisco Durán, Camilo Rocha, José Meseguer

Publication date: 31 January 2020

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2019.100513

zbMATH Keywords

equational programsMaudeorder-sorted specificationsground confluenceinductive joinability proof methodsrewriting modulo axioms

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Symbolic Specialization of Rewriting Logic Theories with Presto, Optimizing Maude programs via program specialization, Unnamed Item, Guest editor's foreword, Programming and symbolic computation in Maude, Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)

Uses Software

• OBJ3
• CafeOBJ
• Maude
• CSI
• CRC 3
• MTT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Strict coherence of conditional rewriting modulo axioms
• Normal forms and normal theories in conditional rewriting
• 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
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• Folding variant narrowing and optimal variant termination
• Specification and proof in membership equational logic
• Proving operational termination of membership equational programs
• CSI: new evidence -- a progress report
• Metalevel algorithms for variant satisfiability
• Semantic foundations for generalized rewrite theories
• Simultaneous checking of completeness and ground confluence for algebraic specifications
• MTT: The Maude Termination Tool (System Description)
• Proving Confluence of Term Rewriting Systems Automatically
• Termination Modulo Combinations of Equational Theories
• Variant-Based Satisfiability in Initial Algebras
• A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications
• Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
• Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications
• Term Rewriting and Applications
• Proving ground confluence of equational specifications modulo axioms