Variant-based decidable satisfiability in initial algebras with predicates

Raúl Gutiérrez, José Meseguer

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

Abstract

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
PublisherSpringer-Verlag Berlin Heidelberg
Pages306-322
Number of pages17
ISBN (Print)9783319944593
DOIs
StatePublished - Jan 1 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

Other

Other27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017
CountryBelgium
CityNamur
Period10/10/1710/12/17

Keywords

  • 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)

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

  • Cite this

    Gutiérrez, R., & Meseguer, J. (2018). Variant-based decidable satisfiability in initial algebras with predicates. In F. Fioravanti, & J. P. Gallagher (Eds.), Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers (pp. 306-322). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10855 LNCS). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-319-94460-9_18