Order-sorted unification
type: Item
instance of: scholarly article
title: Order-sorted unification
zbMATH Open document ID: 0691.03002
DOI: 10.1016/S0747-7171(89)80036-7
author: José Meseguer
author: Joseph Goguen
author: Gert Smolka
published in: Journal of Symbolic Computation
publication date: 1989-01-01T00:00:00Z
review text: Order-sorted equational logic allows a partially ordered set of sorts, the ordering being interpreted as set-theoretic containment in the models. A categorical treatment of unification for such logics is provided. Given \(\Gamma\) (a system of equations) and E (a sort-preserving set of equations, without restrictions on the sorts of its variables), the main results characterize when an order-sorted signature has a minimal (or finite, or, most general, when \(\Gamma\) is decidable) family of order-sorted E-unifiers for \(\Gamma\). For unitary signatures, where each solvable system of equations has a most general unifier, a quasilinear time algorithm for syntactic unification is presented.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 08B05
zbMATH DE Number: 4130340
zbMATH Keywords: Order-sorted equational logic
zbMATH Keywords: categorical treatment of unification
reviewed by: Cristian Masalagiu
MaRDI profile type: Publication
cites work: Q3769958
cites work: An algebraic semantics approach to the effective resolution of type equations
cites work: Cost pass-through and inverse demand curvature in vertical relationships with upstream and downstream competition
cites work: Q4951952
cites work: Complete sets of unifiers and matchers in equational theories
cites work: An Oxford survey of order sorted algebra
cites work: Q3880309
cites work: Q3962973
cites work: Equality, types, modules, and (why not?) generics for logic programming
cites work: Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
cites work: Q3030249
cites work: Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
cites work: Q3719824
cites work: Proofs by induction in equational theories with constructors
cites work: Q3795207
cites work: Q5581665
cites work: Q5639839
cites work: An Efficient Unification Algorithm
cites work: Q3687683
cites work: Q5678447
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q3786020
cites work: Q3992707
cites work: Unification theory
cites work: Q4364536
cites work: Inheritance hierarchies: Semantics and unifications
cites work: A mechanical solution of Schubert's steamroller by many-sorted resolution
cites work: Q3786021
full work available at URL: s0747-7171(89)80036-7
OpenAlex ID: W2031327296
Recommended article: Order-sorted feature theory unification
Recommended article: An ordering linear unification algorithm
Recommended article: Unification in sort theories and its applications
Recommended article: Order-Sorted Generalization
Recommended article: Order-Sorted Unification with Regular Expression Sorts.
Recommended article: Ordering based on uninorms
Recommended article: Q4536326
Recommended article: AC unification through order-sorted AC1 unification
Recommended article: Order-sorted Equational Unification Revisited
description: scientific article; zbMATH DE number 4130340