Associative unification and symbolic reasoning modulo associativity in maude

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

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings
EditorsVlad Rusu
PublisherSpringer-Verlag
Pages98-114
Number of pages17
ISBN (Print)9783319998398
DOIs
StatePublished - Jan 1 2018
Event12th International Workshop on Rewriting Logic and its Applications, WRLA 2018 - Thessaloniki, Greece
Duration: Jun 14 2018Jun 15 2018

Publication series

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

Other

Other12th International Workshop on Rewriting Logic and its Applications, WRLA 2018
CountryGreece
CityThessaloniki
Period6/14/186/15/18

Fingerprint

Maude
Associativity
Unification
Modulo
Reasoning
Symbolic Analysis
Reachability Analysis
Minimal Set
Terminate
Finite Set

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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-Verlag. 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; Martí-Oliet, Narciso; Meseguer, Jose; Talcott, Carolyn.

Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings. ed. / Vlad Rusu. Springer-Verlag, 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 proceedingConference 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-Verlag, 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-Verlag. 2018. p. 98-114. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-99840-4_6
Durán, Francisco ; Eker, Steven ; Escobar, Santiago ; Martí-Oliet, Narciso ; Meseguer, Jose ; Talcott, Carolyn. / 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-Verlag, 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 Jose Meseguer and Carolyn Talcott",
year = "2018",
month = "1",
day = "1",
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-Verlag",
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",

}

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, Jose

AU - Talcott, Carolyn

PY - 2018/1/1

Y1 - 2018/1/1

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

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-Verlag

ER -