Variants in the Infinitary Unification Wonderland

Research output: Chapter in Book/Report/Conference proceedingConference contribution


So far, results about variants, the finite variant property (FVP), and variant unification have been developed for equational theories E∪ B where B is a set of axioms having a finitary unification algorithm, and the equations E, oriented as rewrite rules E→, are convergent modulo B. The extension to the case when B has an infinitary unification algorithm, for example because of non-commutative symbols having associative axioms, seems undeveloped. This paper takes a first step in developing such an extension. In particular, the relationships between the FVP and the boundedness properties, the identification of conditions on E∪ B ensuring FVP, and the effective computation of variants and variant unifiers are explored in detail. The extension from the finitary to the infinitary case includes both surprises and opportunities.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers
EditorsSantiago Escobar, Narciso Martí-Oliet
Number of pages21
ISBN (Print)9783030635947
StatePublished - 2020
Externally publishedYes
Event13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020 - Virtual, Online
Duration: Oct 20 2020Oct 22 2020

Publication series

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


Conference13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020
CityVirtual, Online

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Variants in the Infinitary Unification Wonderland'. Together they form a unique fingerprint.

Cite this