Order-sorted unification (Q582269): Difference between revisions
From MaRDI portal
Created a new Item |
Changed an Item |
||
| Property / 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. | |||
| Property / 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. / rank | |||
Normal rank | |||
| Property / reviewed by | |||
| Property / reviewed by: Q593640 / rank | |||
Normal rank | |||
| Property / Mathematics Subject Classification ID | |||
| Property / Mathematics Subject Classification ID: 03B35 / rank | |||
Normal rank | |||
| Property / Mathematics Subject Classification ID | |||
| Property / Mathematics Subject Classification ID: 08B05 / rank | |||
Normal rank | |||
| Property / zbMATH DE Number | |||
| Property / zbMATH DE Number: 4130340 / rank | |||
Normal rank | |||
| Property / zbMATH Keywords | |||
Order-sorted equational logic | |||
| Property / zbMATH Keywords: Order-sorted equational logic / rank | |||
Normal rank | |||
| Property / zbMATH Keywords | |||
categorical treatment of unification | |||
| Property / zbMATH Keywords: categorical treatment of unification / rank | |||
Normal rank | |||
Revision as of 18:05, 1 July 2023
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Order-sorted unification |
scientific article |
Statements
Order-sorted unification (English)
0 references
1989
0 references
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.
0 references
Order-sorted equational logic
0 references
categorical treatment of unification
0 references
