Variant-Based Satisfiability

Meseguer, José

Permalink

https://hdl.handle.net/2142/88408 Copy

Description

Title

Variant-Based Satisfiability

Author(s)

Meseguer, José

Issue Date

2015-11

Keyword(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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/88408

Sponsor(s)/Grant Number(s)

Partially supported by NSF Grant CNS 13-19109.

Owning Collections