Associative unification and symbolic reasoning modulo associativity in maude

Francisco Durán; Steven Eker; Santiago Escobar; Narciso Martí-Oliet; José Meseguer; Carolyn Talcott

doi:10.1007/978-3-319-99840-4_6

Associative unification and symbolic reasoning modulo associativity in maude

Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott

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

Abstract

We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unification problems u= ^?v such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a finite and complete set of associative unifiers for a fairly large class of unification problems occurring in practice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a warning that such set may be incomplete. This paper describes this associative unification algorithm implemented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrowing based symbolic reachability analysis have been extended to deal with associativity.

Original language	English (US)
Title of host publication	Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings
Editors	Vlad Rusu
Publisher	Springer
Pages	98-114
Number of pages	17
ISBN (Print)	9783319998398
DOIs	https://doi.org/10.1007/978-3-319-99840-4_6
State	Published - 2018
Event	12th International Workshop on Rewriting Logic and its Applications, WRLA 2018 - Thessaloniki, Greece Duration: Jun 14 2018 → Jun 15 2018

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11152 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	12th International Workshop on Rewriting Logic and its Applications, WRLA 2018
Country/Territory	Greece
City	Thessaloniki
Period	6/14/18 → 6/15/18

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-319-99840-4_6

Library availability

Discover UIUC Full Text

Cite this

Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J., & Talcott, C. (2018). Associative unification and symbolic reasoning modulo associativity in maude. In V. Rusu (Ed.), Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings (pp. 98-114). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11152 LNCS). Springer. https://doi.org/10.1007/978-3-319-99840-4_6

Associative unification and symbolic reasoning modulo associativity in maude. / Durán, Francisco; Eker, Steven; Escobar, Santiago et al.
Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings. ed. / Vlad Rusu. Springer, 2018. p. 98-114 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11152 LNCS).

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

Durán, F, Eker, S, Escobar, S, Martí-Oliet, N, Meseguer, J & Talcott, C 2018, Associative unification and symbolic reasoning modulo associativity in maude. in V Rusu (ed.), Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11152 LNCS, Springer, pp. 98-114, 12th International Workshop on Rewriting Logic and its Applications, WRLA 2018, Thessaloniki, Greece, 6/14/18. https://doi.org/10.1007/978-3-319-99840-4_6

Durán F, Eker S, Escobar S, Martí-Oliet N, Meseguer J, Talcott C. Associative unification and symbolic reasoning modulo associativity in maude. In Rusu V, editor, Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings. Springer. 2018. p. 98-114. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-99840-4_6

Durán, Francisco ; Eker, Steven ; Escobar, Santiago et al. / Associative unification and symbolic reasoning modulo associativity in maude. Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings. editor / Vlad Rusu. Springer, 2018. pp. 98-114 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{413c18afcd29474cbb93c2e699bb48f3,

title = "Associative unification and symbolic reasoning modulo associativity in maude",

abstract = "We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unification problems u= ?v such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a finite and complete set of associative unifiers for a fairly large class of unification problems occurring in practice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a warning that such set may be incomplete. This paper describes this associative unification algorithm implemented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrowing based symbolic reachability analysis have been extended to deal with associativity.",

author = "Francisco Dur{\'a}n and Steven Eker and Santiago Escobar and Narciso Mart{\'i}-Oliet and Jos{\'e} Meseguer and Carolyn Talcott",

note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2018.; 12th International Workshop on Rewriting Logic and its Applications, WRLA 2018 ; Conference date: 14-06-2018 Through 15-06-2018",

year = "2018",

doi = "10.1007/978-3-319-99840-4_6",

language = "English (US)",

isbn = "9783319998398",

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

publisher = "Springer",

pages = "98--114",

editor = "Vlad Rusu",

booktitle = "Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings",

address = "Germany",

}

TY - GEN

T1 - Associative unification and symbolic reasoning modulo associativity in maude

AU - Durán, Francisco

AU - Eker, Steven

AU - Escobar, Santiago

AU - Martí-Oliet, Narciso

AU - Meseguer, José

AU - Talcott, Carolyn

PY - 2018

Y1 - 2018

N2 - We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unification problems u= ?v such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a finite and complete set of associative unifiers for a fairly large class of unification problems occurring in practice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a warning that such set may be incomplete. This paper describes this associative unification algorithm implemented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrowing based symbolic reachability analysis have been extended to deal with associativity.

AB - We have added support for associative unification to Maude 2.7.1. Associative unification is infinitary, i.e., there are unification problems u= ?v such that there is an infinite minimal set of unifiers, whereas associative-commutative unification is finitary. A unique feature of the associative unification algorithm implemented in Maude is that it is guaranteed to terminate with a finite and complete set of associative unifiers for a fairly large class of unification problems occurring in practice. For any problems outside this class, the algorithm returns a finite set of unifiers together with a warning that such set may be incomplete. This paper describes this associative unification algorithm implemented in Maude and also how other symbolic reasoning Maude features such as (i) variant generation; (ii) variant unification; and (iii) narrowing based symbolic reachability analysis have been extended to deal with associativity.

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

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

U2 - 10.1007/978-3-319-99840-4_6

DO - 10.1007/978-3-319-99840-4_6

M3 - Conference contribution

AN - SCOPUS:85053911647

SN - 9783319998398

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

SP - 98

EP - 114

BT - Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings

A2 - Rusu, Vlad

PB - Springer

T2 - 12th International Workshop on Rewriting Logic and its Applications, WRLA 2018

Y2 - 14 June 2018 through 15 June 2018

ER -

Associative unification and symbolic reasoning modulo associativity in maude

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this