The dual of most general equational unifiers is that of least general equational anti-unifiers, i.e., most specific anti-instances modulo equations. This work aims to provide a general mechanism for equational anti-unification that leverages the recent advances in variant-based symbolic computation in Maude. Symbolic computation in Maude equational theories is based on folding variant narrowing (FVN), a narrowing strategy that efficiently computes the equational variants of a term (i.e., the irreducible forms of all of its substitution instances). By relying on FVN, we provide an equational anti-unification algorithm that computes the least general anti-unifiers of a term in any equational theory E where the number of least general E-variants is finite for any given term.

Variant-Based Equational Anti-unification

Ballis D.;
2022-01-01

Abstract

The dual of most general equational unifiers is that of least general equational anti-unifiers, i.e., most specific anti-instances modulo equations. This work aims to provide a general mechanism for equational anti-unification that leverages the recent advances in variant-based symbolic computation in Maude. Symbolic computation in Maude equational theories is based on folding variant narrowing (FVN), a narrowing strategy that efficiently computes the equational variants of a term (i.e., the irreducible forms of all of its substitution instances). By relying on FVN, we provide an equational anti-unification algorithm that computes the least general anti-unifiers of a term in any equational theory E where the number of least general E-variants is finite for any given term.
2022
978-3-031-16766-9
978-3-031-16767-6
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/1235270
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact