George Metcalfe ; Leonardo Cabrer - Exact Unification and Admissibility

lmcs:1599 - Logical Methods in Computer Science, September 28, 2015, Volume 11, Issue 3 - https://doi.org/10.2168/LMCS-11(3:23)2015
Exact Unification and AdmissibilityArticle

Authors: George Metcalfe ORCID; Leonardo Cabrer

    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.


    Volume: Volume 11, Issue 3
    Published on: September 28, 2015
    Submitted on: December 23, 2014
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • The roots of plant productivity: how the rhizosphere interact with the aboveground armament for indirect and direct defense against abiotic stressors; Funder: European Commission; Code: 326202
    • Admissible Rules: From Characterizations to Applications; Funder: Swiss National Science Foundation; Code: 146748

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1040 times.
    This article's PDF has been downloaded 430 times.