Extensions of unificationmodulo ACUI

Publikationstyp
Conference Paper
Date Issued
2020-06-01
Sprache
English
Author(s)
Baader, Franz  
Marantidis, Pavlos  
Mottet, Antoine  
Okhotin, Alexander  
TORE-URI
http://hdl.handle.net/11420/12080
Journal
Mathematical structures in computer science  
Volume
30
Issue
6
Start Page
597
End Page
626
Citation
Mathematical Structures in Computer Science 30 (6): 597-626 (2020-06-01)
Publisher DOI
10.1017/S0960129519000185
Scopus ID
2-s2.0-85092705427
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.
Subjects
ACUI
approximate unification
ground identities
Unification theory