Exact unification and admissibility

DOI10.2168/LMCS-11(3:23)2015zbMATH Open1384.08001arXiv1410.5583MaRDI QIDQ3196355FDOQ3196355

Authors: George Metcalfe, Leonardo Manuel Cabrer 

Publication date: 29 October 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: A new hierarchy of "exact" unification types is introduced, motivated by the study of admissibility 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.

Full work available at URL: https://arxiv.org/abs/1410.5583

Recommendations

• The unification hierarchy is undecidable
• Publication:4723704
• scientific article; zbMATH DE number 4041328
• Unification through projectivity
• Essential unifiers

zbMATH Keywords

admissibilityunificationfree algebraequational class

Mathematics Subject Classification ID

Other algebras related to logic (03G25) Equational logic, Mal'tsev conditions (08B05) Free algebras (08B20) Pseudocomplemented lattices (06D15) De Morgan algebras, ?ukasiewicz algebras (lattice-theoretic aspects) (06D30)

Cited In (3)

• Structural and universal completeness in algebra and logic
• UNIFICATION IN SUPERINTUITIONISTIC PREDICATE LOGICS AND ITS APPLICATIONS
• E-Unification based on Generalized Embedding

This page was built for publication: Exact unification and admissibility

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196355)