Variant Narrowing and Equational Unification

Santiago Escobar, José Meseguer, Ralf Sasse

Research output: Contribution to journalArticlepeer-review


Narrowing is a well-known complete procedure for equational E-unification when E can be decomposed as a union E = Δ {multiset union} B with B a set of axioms for which a finitary unification algorithm exists, and Δ a set of confluent, terminating, and B-coherent rewrite rules. However, when B ≠ ∅, effective narrowing strategies such as basic narrowing easily fail to be complete and cannot be used. This poses two challenges to narrowing-based equational unification: (i) finding effective narrowing strategies that are complete modulo B under mild assumptions on B, and (ii) finding sufficient conditions under which such narrowing strategies yield finitary E-unification algorithms. Inspired by Comon and Delaune's notion of E-variant for a term, we propose a new narrowing strategy called variant narrowing that has a search space potentially much smaller than full narrowing, is complete, and yields a finitary E-unification algorithm when E has the finite variant property. We also discuss applications to symbolic reachability analysis of concurrent systems specified as rewrite theories, and in particular to the formal analysis of cryptographic protocols modulo the algebraic properties of the underlying cryptographic functions.

Original languageEnglish (US)
Pages (from-to)103-119
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
Issue number3
StatePublished - Jun 29 2009


  • Equational unification
  • cryptographic protocol analysis
  • finite variant property
  • narrowing
  • symbolic reachability analysis

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Variant Narrowing and Equational Unification'. Together they form a unique fingerprint.

Cite this