Variant-based satisfiability in initial algebras

José Meseguer

doi:10.1007/978-3-319-29510-7_1

Variant-based satisfiability in initial algebras

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Formal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers
Editors	Peter Csaba Ölveczky, Cyrille Artho
Publisher	Springer
Pages	3-34
Number of pages	32
ISBN (Print)	9783319295091
DOIs	https://doi.org/10.1007/978-3-319-29510-7_1
State	Published - 2016
Event	4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015 - Paris, France Duration: Nov 6 2015 → Nov 7 2015

Publication series

Name	Communications in Computer and Information Science
Volume	596
ISSN (Print)	1865-0929

Other

Other	4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015
Country/Territory	France
City	Paris
Period	11/6/15 → 11/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)

Online availability

10.1007/978-3-319-29510-7_1

Library availability

Discover UIUC Full Text

Cite this

Variant-based satisfiability in initial algebras. / Meseguer, José.
Formal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers. ed. / Peter Csaba Ölveczky; Cyrille Artho. Springer, 2016. p. 3-34 (Communications in Computer and Information Science; Vol. 596).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Meseguer, J 2016, Variant-based satisfiability in initial algebras. in PC Ölveczky & C Artho (eds), Formal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers. Communications in Computer and Information Science, vol. 596, Springer, pp. 3-34, 4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015, Paris, France, 11/6/15. https://doi.org/10.1007/978-3-319-29510-7_1

@inproceedings{d781b8fb5d3e4a75a5e3bc51cee8da8a,

title = "Variant-based 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{\textquoteright}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.",

keywords = "Constructor unifier, Constructor variant, Finite variant property (FVP), Folding variant narrowing, Satisfiability in initial algebras",

author = "Jos{\'e} Meseguer",

year = "2016",

doi = "10.1007/978-3-319-29510-7_1",

language = "English (US)",

isbn = "9783319295091",

series = "Communications in Computer and Information Science",

publisher = "Springer",

pages = "3--34",

editor = "{\"O}lveczky, {Peter Csaba} and Cyrille Artho",

booktitle = "Formal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers",

address = "Germany",

note = "4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015 ; Conference date: 06-11-2015 Through 07-11-2015",

}

TY - GEN

T1 - Variant-based satisfiability in initial algebras

AU - Meseguer, José

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

KW - Constructor unifier

KW - Constructor variant

KW - Finite variant property (FVP)

KW - Folding variant narrowing

KW - Satisfiability in initial algebras

UR - http://www.scopus.com/inward/record.url?scp=84958968100&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84958968100&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-29510-7_1

DO - 10.1007/978-3-319-29510-7_1

M3 - Conference contribution

AN - SCOPUS:84958968100

SN - 9783319295091

T3 - Communications in Computer and Information Science

SP - 3

EP - 34

BT - Formal Techniques for Safety-Critical Systems - 4th International Workshop, FTSCS 2015, Revised Selected Papers

A2 - Ölveczky, Peter Csaba

A2 - Artho, Cyrille

PB - Springer

T2 - 4th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2015

Y2 - 6 November 2015 through 7 November 2015

ER -

Variant-based satisfiability in initial algebras

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this