Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*

DOI10.3233/FI-2020-1991zbMath1497.68235arXiv1808.05097MaRDI QIDQ4988927

José Meseguer, A. Cuenca-Ortega, Santiago Escobar, María Alpuente

Publication date: 20 May 2021

Published in: Fundamenta Informaticae, Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1808.05097

zbMATH Keywords

rewriting logicMaudehomeomorphic embedding

Mathematics Subject Classification ID

Logic in computer science (03B70) Applications of universal algebra in computer science (08A70) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (9)

E-Unification based on Generalized Embedding ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Optimizing Maude programs via program specialization ⋮ Programming and symbolic computation in Maude ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms* ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Symbolic computation in Maude: some tapas

Uses Software

• Maude
• PROC POWER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exploring conditional rewriting logic computations
• Strict coherence of conditional rewriting modulo axioms
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• A note on simplification orderings
• Conditional rewriting logic as a unified model of concurrency
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Simple termination is difficult
• Single elementary associative-commutative matching
• Reflection in conditional rewriting logic
• On equational theories, unification, and (un)decidability
• Folding variant narrowing and optimal variant termination
• Specification and proof in membership equational logic
• Partial evaluation of order-sorted equational programs modulo axioms
• The theory of well-quasi-ordering: a frequently discovered concept
• Order-Sorted Rewriting and Congruence Closure
• Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture

This page was built for publication: Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*