Extensions of unificationmodulo ACUI

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F19%3A10401391" target="_blank" >RIV/00216208:11320/19:10401391 - isvavai.cz</a>
Result on the web
<a href="https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=FewD6L6rkB" target="_blank" >https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=FewD6L6rkB</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1017/S0960129519000185" target="_blank" >10.1017/S0960129519000185</a>

Result language
angličtina
Original language name
Extensions of unificationmodulo ACUI
Original language description
The theory ACUI of an associative, commutative, and idempotent binary function symbol + with unit 0 was one of the first equational theories for which the complexity of testing solvability of unification problems was investigated in detail. In this paper, we investigate two extensions of ACUI. On one hand, we consider approximate ACUI-unification, where we use appropriate measures to express how close a substitution is to being a unifier. On the other hand, we extend ACUI-unification to ACUIG-unification, that is, unification in equational theories that are obtained from ACUI by adding a finite set G of ground identities. Finally, we combine the two extensions, that is, consider approximate ACUI-unification. For all cases we are able to determine the exact worst-case complexity of the unification problem.
Czech name
—
Czech description
—

Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year
2019
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)