Standard

Extensions of unification modulo ACUI. / Baader, Franz; Marantidis, Pavlos; Mottet, Antoine; Okhotin, Alexander.

In: Mathematical Structures in Computer Science, Vol. 30, No. 6, 01.06.2020, p. 597-626.

Research output: Contribution to journal › Article › peer-review

Harvard

Baader, F, Marantidis, P, Mottet, A & Okhotin, A 2020, 'Extensions of unification modulo ACUI', Mathematical Structures in Computer Science, vol. 30, no. 6, pp. 597-626. https://doi.org/10.1017/S0960129519000185

APA

Baader, F., Marantidis, P., Mottet, A., & Okhotin, A. (2020). Extensions of unification modulo ACUI. Mathematical Structures in Computer Science, 30(6), 597-626. https://doi.org/10.1017/S0960129519000185

Vancouver

Baader F, Marantidis P, Mottet A, Okhotin A. Extensions of unification modulo ACUI. Mathematical Structures in Computer Science. 2020 Jun 1;30(6):597-626. https://doi.org/10.1017/S0960129519000185

Author

Baader, Franz ; Marantidis, Pavlos ; Mottet, Antoine ; Okhotin, Alexander. / Extensions of unification modulo ACUI. In: Mathematical Structures in Computer Science. 2020 ; Vol. 30, No. 6. pp. 597-626.

BibTeX

@article{357ad33c56b04c2aa263decfcf81c09c,
title = "Extensions of unification modulo ACUI",
abstract = "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. ",
keywords = "ACUI, approximate unification, ground identities, Unification theory, SET",
author = "Franz Baader and Pavlos Marantidis and Antoine Mottet and Alexander Okhotin",
note = "Funding Information: Supported by DFG Graduiertenkolleg 1763 (QuantLA). ‡ Funding Information: Partially supported by DFG Graduiertenkolleg 1763 (QuantLA). Publisher Copyright: {\textcopyright} Copyright: Copyright 2020 Elsevier B.V., All rights reserved.",
year = "2020",
month = jun,
day = "1",
doi = "10.1017/S0960129519000185",
language = "English",
volume = "30",
pages = "597--626",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
publisher = "Cambridge University Press",
number = "6",

}

RIS

TY - JOUR

T1 - Extensions of unification modulo ACUI

AU - Baader, Franz

AU - Marantidis, Pavlos

AU - Mottet, Antoine

AU - Okhotin, Alexander

N1 - Funding Information: Supported by DFG Graduiertenkolleg 1763 (QuantLA). ‡ Funding Information: Partially supported by DFG Graduiertenkolleg 1763 (QuantLA). Publisher Copyright: © Copyright: Copyright 2020 Elsevier B.V., All rights reserved.

PY - 2020/6/1

Y1 - 2020/6/1

N2 - 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.

AB - 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.

KW - ACUI

KW - approximate unification

KW - ground identities

KW - Unification theory

KW - SET

UR - http://www.scopus.com/inward/record.url?scp=85092705427&partnerID=8YFLogxK

UR - https://www.mendeley.com/catalogue/7e31072a-63ed-3ec3-8b5c-52f52088c54b/

U2 - 10.1017/S0960129519000185

DO - 10.1017/S0960129519000185

M3 - Article

AN - SCOPUS:85092705427

VL - 30

SP - 597

EP - 626

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 6

ER -

ID: 70816165