Most General Variant Unifiers
Santiago Escobar (VRAIN, Valencian Research Institute for Artificial, Intelligence, Universitat Polit\`ecnica de Val\`encia), Julia Sapi\~na, (VRAIN, Valencian Research Institute for Artificial Intelligence, Universitat, Polit\`ecnica de Val\`encia)

TL;DR
This paper enhances a variant-based equational unification algorithm in Maude to produce minimal, most general unifiers, improving efficiency in execution time and the number of unifiers computed.
Contribution
It introduces a strengthened variant-based unification algorithm that yields minimal, most general unifiers, optimizing the existing Maude implementation.
Findings
More efficient unification in Maude with fewer unifiers
Algorithm produces minimal, most general variant unifiers
Experimental results show improved performance
Abstract
Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. Equational unification is of special relevance to automated deduction, theorem proving, protocol analysis, partial evaluation, model checking, etc. Several algorithms have been developed in the literature for specific equational theories, such as associative-commutative symbols, exclusive-or, Diffie-Hellman, or Abelian Groups. Narrowing was proved to be complete for unification and several cases have been studied where narrowing provides a decidable unification algorithm. A new narrowing-based equational unification algorithm relying on the concept of the variants of a term has been developed and it is available in the most recent version of Maude, version 2.7.1, which provides quite sophisticated unification features. A variant of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Advanced Database Systems and Queries · Formal Methods in Verification
