Metcalfe, George; Cabrer, Leonardo Manuel (2015). Exact Unification and Admissibility. Logical methods in computer science, 11(3), pp. 1-15. Department of Theoretical Computer Science, Technical University of Braunschweig 10.2168/LMCS-11(3:23)2015
|
Text
1508.04360.pdf - Published Version Available under License Creative Commons: Attribution-No Derivative Works (CC-BY-ND). Download (220kB) | Preview |
A new hierarchy of "exact" unification types is introduced, motivated by the study of admissible rules for equational classes and non-classical logics. In this setting, unifiers of identities in an equational class are preordered, not by instantiation, but rather by inclusion over the corresponding sets of unified identities. Minimal complete sets of unifiers under this new preordering always have a smaller or equal cardinality than those provided by the standard instantiation preordering, and in significant cases a dramatic reduction may be observed. In particular, the classes of distributive lattices, idempotent semigroups, and MV-algebras, which all have nullary unification type, have unitary or finitary exact type. These results are obtained via an algebraic interpretation of exact unification, inspired by Ghilardi's algebraic approach to equational unification.
Item Type: |
Journal Article (Original Article) |
|---|---|
Division/Institute: |
08 Faculty of Science > Department of Mathematics and Statistics > Institute of Mathematics |
UniBE Contributor: |
Metcalfe, George, Cabrer, Leonardo Manuel |
Subjects: |
500 Science > 510 Mathematics |
ISSN: |
1860-5974 |
Publisher: |
Department of Theoretical Computer Science, Technical University of Braunschweig |
Language: |
English |
Submitter: |
George Metcalfe |
Date Deposited: |
07 Jan 2016 15:31 |
Last Modified: |
05 Dec 2022 14:50 |
Publisher DOI: |
10.2168/LMCS-11(3:23)2015 |
BORIS DOI: |
10.7892/boris.74480 |
URI: |
https://boris.unibe.ch/id/eprint/74480 |
Actions (login required)
 |
Edit item |