Files in this item



application/pdfvar-sat.pdf (656kB)
(no description provided)PDF


Title:Variant-Based Satisfiability
Author(s):Jose Meseguer
Subject(s):finite variant property (FVP)
constructor variant
constructor unifier
folding variant narrowing
satisfiability in initial algebras
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 variant-based satisfiability are identified, and a method based on descent maps to bring other theories into these classes and to improve the generic algorithm's efficiency is proposed and illustrated with examples.
Issue Date:2015-11
Genre:Technical Report
Sponsor:Partially supported by NSF Grant CNS 13-19109.
Date Available in IDEALS:2015-11-14

This item appears in the following Collection(s)

Item Statistics