The Unification Type of ACUI w.r.t. the Unrestricted Instantiation Preorder is not Finitary

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Contributors

Abstract

The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. It is known that the unification type of an equational theory may vary, depending on which instantiation preorder is used. More precisely, it was shown that the theory ACUI of an associative, commutative, and idempotent binary function symbol with a unit is unitary w.r.t. the restricted instantiation preorder, but not unitary w.r.t. the unrestricted one. Here, we improve on this result, by showing that, w.r.t. the unrestricted instantiation preorder, ACUI is not even finitary.

Details

Original languageEnglish
Title of host publicationProceedings of the 30th International Workshop on Unification (UNIF'16)
Pages31-35
Number of pages5
Publication statusPublished - 2016
Peer-reviewedYes

External IDs

ORCID /0000-0002-4049-221X/work/142247960

Keywords