Equational formulas and pattern operations in initial order-sorted algebras

DOI10.1007/s00165-017-0415-5zbMath1362.68054OpenAlexW2586953020MaRDI QIDQ2628298

Stephen Skeirik, José Meseguer

Publication date: 1 June 2017

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-017-0415-5

zbMATH Keywords

order-sorted logicinitial decidabilitypattern operations

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Theory of programming languages (68N15) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

A complete semantics of \(\mathbb{K}\) and its translation to Isabelle, Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras, Generalized rewrite theories, coherence completion, and symbolic methods, Programming and symbolic computation in Maude

Uses Software

• Haskell
• OBJ3
• CafeOBJ
• Maude

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Order-sorted unification
• Equational abstractions
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Explicit representation of terms defined by counter examples
• Equational problems and disunification
• Conditional rewriting logic as a unified model of concurrency
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Negation elimination in empty or permutative theories
• Equational formulae with membership constraints
• Explicit versus implicit representations of subsets of the Herbrand universe.
• A modular order-sorted equational generalization algorithm
• Language Prototyping: An Algebraic Specification Approach
• Institutions: abstract model theory for specification and programming
• Variant-Based Satisfiability in Initial Algebras
• The negation elimination from syntactic equational formula is decidable
• Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras