Unification modulo lists with reverse relation with certain word equations

Siva Anantharaman; Peter Hibbs; Paliath Narendran; Michael Rusinowitch

doi:10.1007/978-3-030-29436-6_1

Unification modulo lists with reverse relation with certain word equations

Siva Anantharaman
, Peter Hibbs
, Paliath Narendran
, Michael Rusinowitch

Computer Science

University at Albany

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

Abstract

Decision procedures for various list theories have been investigated in the literature with applications to automated verification. Here we show that the unifiability problem for some list theories with a reverse operator is NP-complete. We also give a unifiability algorithm for the case where the theories are extended with a length operator on lists.

Original language	English
Title of host publication	Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings
Editors	Pascal Fontaine
Publisher	Springer
Pages	1-17
Number of pages	17
ISBN (Print)	9783030294359
DOIs	https://doi.org/10.1007/978-3-030-29436-6_1
State	Published - 2019
Event	27th International Conference on Automated Deduction, CADE 2019 - Natal, Brazil Duration: Aug 27 2019 → Aug 30 2019

Publication series

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

Conference

Conference	27th International Conference on Automated Deduction, CADE 2019
Country/Territory	Brazil
City	Natal
Period	08/27/19 → 08/30/19

Access to Document

10.1007/978-3-030-29436-6_1

Cite this

Anantharaman, S., Hibbs, P., Narendran, P., & Rusinowitch, M. (2019). Unification modulo lists with reverse relation with certain word equations. In P. Fontaine (Ed.), Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings (pp. 1-17). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11716 LNAI). Springer. https://doi.org/10.1007/978-3-030-29436-6_1

Anantharaman, Siva ; Hibbs, Peter ; Narendran, Paliath et al. / Unification modulo lists with reverse relation with certain word equations. Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings. editor / Pascal Fontaine. Springer, 2019. pp. 1-17 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6cec6f932dac4d53a47f4679d3cd6e19,

title = "Unification modulo lists with reverse relation with certain word equations",

abstract = "Decision procedures for various list theories have been investigated in the literature with applications to automated verification. Here we show that the unifiability problem for some list theories with a reverse operator is NP-complete. We also give a unifiability algorithm for the case where the theories are extended with a length operator on lists.",

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

note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2019.; 27th International Conference on Automated Deduction, CADE 2019 ; Conference date: 27-08-2019 Through 30-08-2019",

year = "2019",

doi = "10.1007/978-3-030-29436-6\_1",

language = "English",

isbn = "9783030294359",

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

publisher = "Springer",

pages = "1--17",

editor = "Pascal Fontaine",

booktitle = "Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings",

}

Anantharaman, S, Hibbs, P, Narendran, P & Rusinowitch, M 2019, Unification modulo lists with reverse relation with certain word equations. in P Fontaine (ed.), Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11716 LNAI, Springer, pp. 1-17, 27th International Conference on Automated Deduction, CADE 2019, Natal, Brazil, 08/27/19. https://doi.org/10.1007/978-3-030-29436-6_1

Unification modulo lists with reverse relation with certain word equations. / Anantharaman, Siva; Hibbs, Peter; Narendran, Paliath et al.
Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings. ed. / Pascal Fontaine. Springer, 2019. p. 1-17 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11716 LNAI).

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

TY - GEN

T1 - Unification modulo lists with reverse relation with certain word equations

AU - Anantharaman, Siva

AU - Hibbs, Peter

AU - Narendran, Paliath

AU - Rusinowitch, Michael

PY - 2019

Y1 - 2019

N2 - Decision procedures for various list theories have been investigated in the literature with applications to automated verification. Here we show that the unifiability problem for some list theories with a reverse operator is NP-complete. We also give a unifiability algorithm for the case where the theories are extended with a length operator on lists.

AB - Decision procedures for various list theories have been investigated in the literature with applications to automated verification. Here we show that the unifiability problem for some list theories with a reverse operator is NP-complete. We also give a unifiability algorithm for the case where the theories are extended with a length operator on lists.

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

U2 - 10.1007/978-3-030-29436-6_1

DO - 10.1007/978-3-030-29436-6_1

M3 - Conference contribution

SN - 9783030294359

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

SP - 1

EP - 17

BT - Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings

A2 - Fontaine, Pascal

PB - Springer

T2 - 27th International Conference on Automated Deduction, CADE 2019

Y2 - 27 August 2019 through 30 August 2019

ER -

Anantharaman S, Hibbs P, Narendran P, Rusinowitch M. Unification modulo lists with reverse relation with certain word equations. In Fontaine P, editor, Automated Deduction – CADE 2019- 27th International Conference on Automated Deduction, Proceedings. Springer. 2019. p. 1-17. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-29436-6_1

Unification modulo lists with reverse relation with certain word equations

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this