Unification modulo ACUI plus homomorphisms/distributivity

Siva Anantharaman; Paliath Narendran; Michael Rusinowitch

doi:10.1007/978-3-540-45085-6_38

Unification modulo ACUI plus homomorphisms/distributivity

Siva Anantharaman
, Paliath Narendran
, Michael Rusinowitch

Computer Science

University at Albany

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

In this paper, we consider the unification problem over theories that are extensions of ACI or ACUI, obtained by adding finitely many homomorphism symbols, or a symbol ‘∗’ that distributes over the ACUI-symbol denoted ‘+’. We first show that when we adjoin a set of commuting homomorphisms to ACUI, unification is undecidable. We then consider the ACUIDl-unification problem, i.e., unification modulo ACUI plus left-distributivity of a given ‘∗’ w.r.t. ‘+’, and prove its NEXPTIME-decidability. When we assume the symbol ‘∗’ to be 2-sided distributive w.r.t. ‘+’, we get the theory ACUID, for which the unification problem remains decidable. But when equations of associativitycommutativity, or just of associativity, on ‘∗’ are added on to ACUID, the unification problem becomes undecidable.

Original language	English
Title of host publication	Automated Deduction - CADE-19 - 19th International Conference on Automated Deduction, Proceedings
Editors	Franz Baader
Publisher	Springer Verlag
Pages	442-457
Number of pages	16
ISBN (Print)	3540405593, 9783540405597
DOIs	https://doi.org/10.1007/978-3-540-45085-6_38
State	Published - 2003
Event	19th International Conference on Automated Deduction, CADE 2003 - Miami Beach, United States Duration: Jul 28 2003 → Aug 2 2003

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2741

Conference

Conference	19th International Conference on Automated Deduction, CADE 2003
Country/Territory	United States
City	Miami Beach
Period	07/28/03 → 08/2/03

Keywords

Complexity
E-Unification
Minsky machine
Post correspondence problem
Rewrite reachability
Set constraints

Access to Document

10.1007/978-3-540-45085-6_38

Cite this

Anantharaman, S., Narendran, P., & Rusinowitch, M. (2003). Unification modulo ACUI plus homomorphisms/distributivity. In F. Baader (Ed.), Automated Deduction - CADE-19 - 19th International Conference on Automated Deduction, Proceedings (pp. 442-457). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2741). Springer Verlag. https://doi.org/10.1007/978-3-540-45085-6_38

Anantharaman, Siva ; Narendran, Paliath ; Rusinowitch, Michael. / Unification modulo ACUI plus homomorphisms/distributivity. Automated Deduction - CADE-19 - 19th International Conference on Automated Deduction, Proceedings. editor / Franz Baader. Springer Verlag, 2003. pp. 442-457 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{47f434069ba04a87af720e62704c6079,

title = "Unification modulo ACUI plus homomorphisms/distributivity",

abstract = "In this paper, we consider the unification problem over theories that are extensions of ACI or ACUI, obtained by adding finitely many homomorphism symbols, or a symbol {\textquoteleft}∗{\textquoteright} that distributes over the ACUI-symbol denoted {\textquoteleft}+{\textquoteright}. We first show that when we adjoin a set of commuting homomorphisms to ACUI, unification is undecidable. We then consider the ACUIDl-unification problem, i.e., unification modulo ACUI plus left-distributivity of a given {\textquoteleft}∗{\textquoteright} w.r.t. {\textquoteleft}+{\textquoteright}, and prove its NEXPTIME-decidability. When we assume the symbol {\textquoteleft}∗{\textquoteright} to be 2-sided distributive w.r.t. {\textquoteleft}+{\textquoteright}, we get the theory ACUID, for which the unification problem remains decidable. But when equations of associativitycommutativity, or just of associativity, on {\textquoteleft}∗{\textquoteright} are added on to ACUID, the unification problem becomes undecidable.",

keywords = "Complexity, E-Unification, Minsky machine, Post correspondence problem, Rewrite reachability, Set constraints",

author = "Siva Anantharaman and Paliath Narendran and Michael Rusinowitch",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2003.; 19th International Conference on Automated Deduction, CADE 2003 ; Conference date: 28-07-2003 Through 02-08-2003",

year = "2003",

doi = "10.1007/978-3-540-45085-6\_38",

language = "English",

isbn = "3540405593",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "442--457",

editor = "Franz Baader",

booktitle = "Automated Deduction - CADE-19 - 19th International Conference on Automated Deduction, Proceedings",

}

Anantharaman, S, Narendran, P & Rusinowitch, M 2003, Unification modulo ACUI plus homomorphisms/distributivity. in F Baader (ed.), Automated Deduction - CADE-19 - 19th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2741, Springer Verlag, pp. 442-457, 19th International Conference on Automated Deduction, CADE 2003, Miami Beach, United States, 07/28/03. https://doi.org/10.1007/978-3-540-45085-6_38

Unification modulo ACUI plus homomorphisms/distributivity. / Anantharaman, Siva; Narendran, Paliath; Rusinowitch, Michael.
Automated Deduction - CADE-19 - 19th International Conference on Automated Deduction, Proceedings. ed. / Franz Baader. Springer Verlag, 2003. p. 442-457 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2741).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Unification modulo ACUI plus homomorphisms/distributivity

AU - Anantharaman, Siva

AU - Narendran, Paliath

AU - Rusinowitch, Michael

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2003.

PY - 2003

Y1 - 2003

N2 - In this paper, we consider the unification problem over theories that are extensions of ACI or ACUI, obtained by adding finitely many homomorphism symbols, or a symbol ‘∗’ that distributes over the ACUI-symbol denoted ‘+’. We first show that when we adjoin a set of commuting homomorphisms to ACUI, unification is undecidable. We then consider the ACUIDl-unification problem, i.e., unification modulo ACUI plus left-distributivity of a given ‘∗’ w.r.t. ‘+’, and prove its NEXPTIME-decidability. When we assume the symbol ‘∗’ to be 2-sided distributive w.r.t. ‘+’, we get the theory ACUID, for which the unification problem remains decidable. But when equations of associativitycommutativity, or just of associativity, on ‘∗’ are added on to ACUID, the unification problem becomes undecidable.

AB - In this paper, we consider the unification problem over theories that are extensions of ACI or ACUI, obtained by adding finitely many homomorphism symbols, or a symbol ‘∗’ that distributes over the ACUI-symbol denoted ‘+’. We first show that when we adjoin a set of commuting homomorphisms to ACUI, unification is undecidable. We then consider the ACUIDl-unification problem, i.e., unification modulo ACUI plus left-distributivity of a given ‘∗’ w.r.t. ‘+’, and prove its NEXPTIME-decidability. When we assume the symbol ‘∗’ to be 2-sided distributive w.r.t. ‘+’, we get the theory ACUID, for which the unification problem remains decidable. But when equations of associativitycommutativity, or just of associativity, on ‘∗’ are added on to ACUID, the unification problem becomes undecidable.

KW - Complexity

KW - E-Unification

KW - Minsky machine

KW - Post correspondence problem

KW - Rewrite reachability

KW - Set constraints

UR - https://www.scopus.com/pages/publications/7044229280

U2 - 10.1007/978-3-540-45085-6_38

DO - 10.1007/978-3-540-45085-6_38

M3 - Conference contribution

SN - 3540405593

SN - 9783540405597

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 442

EP - 457

BT - Automated Deduction - CADE-19 - 19th International Conference on Automated Deduction, Proceedings

A2 - Baader, Franz

PB - Springer Verlag

T2 - 19th International Conference on Automated Deduction, CADE 2003

Y2 - 28 July 2003 through 2 August 2003

ER -

Anantharaman S, Narendran P, Rusinowitch M. Unification modulo ACUI plus homomorphisms/distributivity. In Baader F, editor, Automated Deduction - CADE-19 - 19th International Conference on Automated Deduction, Proceedings. Springer Verlag. 2003. p. 442-457. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-45085-6_38

Unification modulo ACUI plus homomorphisms/distributivity

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this