Order-sorted unification

DOI10.1016/S0747-7171(89)80036-7zbMath0691.03002OpenAlexW2031327296MaRDI QIDQ582269

Joseph A. Goguen, Gert Smolka, José Meseguer

Publication date: 1989

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0747-7171(89)80036-7

zbMATH Keywords

categorical treatment of unificationOrder-sorted equational logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational logic, Mal'tsev conditions (08B05)

Related Items

A complete semantics of \(\mathbb{K}\) and its translation to Isabelle ⋮ Unique-sort order-sorted theories : A description as monad morphisms ⋮ Higher-order unification, polymorphism, and subsorts ⋮ Equational formulas and pattern operations in initial order-sorted algebras ⋮ Order-Sorted Parameterization and Induction ⋮ Unification in sort theories and its applications ⋮ On First-Order Model-Based Reasoning ⋮ A modular order-sorted equational generalization algorithm ⋮ The calculus of context relations ⋮ A Higher-Order Calculus of Computational Fields ⋮ Unnamed Item ⋮ Semantics of order-sorted specifications ⋮ Strict coherence of conditional rewriting modulo axioms ⋮ Order-sorted Equational Unification Revisited ⋮ Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras ⋮ Completion of rewrite systems with membership constraints ⋮ Programming and symbolic computation in Maude ⋮ On notions of inductive validity for first-order equational clauses ⋮ Regular expression order-sorted unification and matching ⋮ Order-Sorted Generalization ⋮ Symbolic computation in Maude: some tapas

Cites Work

• Cost pass-through and inverse demand curvature in vertical relationships with upstream and downstream competition
• Proofs by induction in equational theories with constructors
• A mechanical solution of Schubert's steamroller by many-sorted resolution
• An algebraic semantics approach to the effective resolution of type equations
• Inheritance hierarchies: Semantics and unifications
• Unification theory
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
• Complete sets of unifiers and matchers in equational theories
• An Efficient Unification Algorithm
• An Oxford survey of order sorted algebra
• A Machine-Oriented Logic Based on the Resolution Principle
• Equality, types, modules, and (why not?) generics for logic programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item