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 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 Berlin Heidelberg
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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Associative unification and symbolic reasoning modulo associativity in maude'. Together they form a unique fingerprint.

  • 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 Berlin Heidelberg. https://doi.org/10.1007/978-3-319-99840-4_6