Metalevel algorithms for variant satisfiability

Stephen Skeirik, José Meseguer

Research output: Contribution to journalArticlepeer-review


Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra TΣ/E when the theory (Σ,E) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation of variant satisfiability checking using these sub-algorithms in Maude 2.7.1.

Original languageEnglish (US)
Pages (from-to)81-110
Number of pages30
JournalJournal of Logical and Algebraic Methods in Programming
StatePublished - Apr 2018


  • Finite variant property (FVP)
  • Folding variant narrowing
  • Maude
  • Metalevel algorithms
  • Reflection
  • Satisfiability in initial algebras

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Software
  • Logic
  • Computational Theory and Mathematics


Dive into the research topics of 'Metalevel algorithms for variant satisfiability'. Together they form a unique fingerprint.

Cite this