Variant-based decidable satisfiability in initial algebras with predicates

Raúl Gutiérrez, José Meseguer

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


Decision procedures can be either theory-specific, e.g., Presburger arithmetic, or theory-generic, applying to an infinite number of user-definable theories. Variant satisfiability is a theory-generic procedure for quantifier-free satisfiability in the initial algebra of an order-sorted equational theory (Σ, E∪B) under two conditions: (i) E∪B has the finite variant property and B has a finitary unification algorithm; and (ii) (Σ, E∪B) protects a constructor subtheory (Ω,EΩ ∪ B_Ω) that is OS-compact. These conditions apply to many user-definable theories, but have a main limitation: they apply well to data structures, but often do not hold for user-definable predicates on such data structures. We present a theory-generic satisfiability decision procedure, and a prototype implementation, extending variant-based satisfiability to initial algebras with user-definable predicates under fairly general conditions.

Original languageEnglish (US)
Title of host publicationLogic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers
EditorsFabio Fioravanti, John P. Gallagher
Number of pages17
ISBN (Print)9783319944593
StatePublished - 2018
Event27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017 - Namur, Belgium
Duration: Oct 10 2017Oct 12 2017

Publication series

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


Other27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017


  • Decidable validity and satisfiability
  • Finite variant property (fvp)
  • OS-compactness
  • User-definable predicates
  • in initial algebras

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this