Variant-based satisfiability in initial algebras

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


Although different satisfiability decision procedures can be combined by algorithms such as those of Nelson-Oppen or Shostak, current tools typically can only support a finite number of theories to use in such combinations. To make SMT solving more widely applicable, generic satisfiability algorithms that can allow a potentially infinite number of decidable theories to be user-definable, instead of needing to be built in by the implementers, are highly desirable. This work studies how folding variant narrowing, a generic unification algorithm that offers good extensibility in unification theory, can be extended to a generic variant- based, satisfiability algorithm for the initial algebras of its user-specified input theories when such theories satisfy Comon-Delaune’s finite variant property (FVP) and some extra conditions. Several, increasingly larger infinite classes of theories whose initial algebras enjoy decidable variantbased satisfiability are identified and illustrated with examples.

Original languageEnglish (US)
Title of host publicationFormal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers
EditorsPeter Csaba Ölveczky, Cyrille Artho
Number of pages32
ISBN (Print)9783319295091
StatePublished - 2016
Event4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015 - Paris, France
Duration: Nov 6 2015Nov 7 2015

Publication series

NameCommunications in Computer and Information Science
ISSN (Print)1865-0929


Other4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015


  • Constructor unifier
  • Constructor variant
  • Finite variant property (FVP)
  • Folding variant narrowing
  • Satisfiability in initial algebras

ASJC Scopus subject areas

  • Computer Science(all)
  • Mathematics(all)


Dive into the research topics of 'Variant-based satisfiability in initial algebras'. Together they form a unique fingerprint.

Cite this