The Unification Type of ACUI w.r.t. the Unrestricted Instantiation Preorder is not Finitary
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-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 language | English |
---|---|
Title of host publication | Proceedings of the 30th International Workshop on Unification (UNIF'16) |
Pages | 31-35 |
Number of pages | 5 |
Publication status | Published - 2016 |
Peer-reviewed | Yes |
External IDs
ORCID | /0000-0002-4049-221X/work/142247960 |
---|