Paper Info
Title
Extensions of unification modulo ACUI.
Abstract
The theory ACUI of an associative, commutative, and idempotent binary function symbol + with unit0was 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 setGof 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.
Year
DOI
Venue
2020
10.1017/S0960129519000185
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE
Keywords
DocType
Volume
Unification theory,ACUI,approximate unification,ground identities
Journal
30
Issue
ISSN
Citations 
SP6
0960-1295
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Franz Baader18123646.64
Pavlos Marantidis202.03
Antoine Mottet3207.45
Alexander Okhotin481574.63