Order-sorted unification (Q582269)

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.