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

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Beitragende

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

OriginalspracheEnglisch
TitelProceedings of the 30th International Workshop on Unification (UNIF'16)
Seiten31-35
Seitenumfang5
PublikationsstatusVeröffentlicht - 2016
Peer-Review-StatusJa

Externe IDs

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

Schlagworte