Variant-based satisfiability in initial algebras

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

Abstract

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
PublisherSpringer-Verlag Berlin Heidelberg
Pages3-34
Number of pages32
ISBN (Print)9783319295091
DOIs
StatePublished - Jan 1 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
Volume596
ISSN (Print)1865-0929

Other

Other4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015
CountryFrance
CityParis
Period11/6/1511/7/15

Keywords

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

ASJC Scopus subject areas

  • Computer Science(all)
  • Mathematics(all)

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

  • Cite this

    Meseguer, J. (2016). Variant-based satisfiability in initial algebras. In P. C. Ölveczky, & C. Artho (Eds.), Formal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers (pp. 3-34). (Communications in Computer and Information Science; Vol. 596). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-319-29510-7_1