Metalevel algorithms for variant satisfiability

Stephen Skeirik; José Meseguer

doi:10.1016/j.jlamp.2017.12.006

Metalevel algorithms for variant satisfiability

Research output: Contribution to journal › Article › peer-review

Abstract

Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra T_Σ/E when the theory (Σ,E) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation of variant satisfiability checking using these sub-algorithms in Maude 2.7.1.

Original language	English (US)
Pages (from-to)	81-110
Number of pages	30
Journal	Journal of Logical and Algebraic Methods in Programming
Volume	96
DOIs	https://doi.org/10.1016/j.jlamp.2017.12.006
State	Published - Apr 2018

Keywords

Finite variant property (FVP)
Folding variant narrowing
Maude
Metalevel algorithms
Reflection
Satisfiability in initial algebras

ASJC Scopus subject areas

Theoretical Computer Science
Software
Logic
Computational Theory and Mathematics

Online availability

10.1016/j.jlamp.2017.12.006

Library availability

Discover UIUC Full Text

Cite this

@article{09fea4c671f14888947b8c482fee43b6,

title = "Metalevel algorithms for variant satisfiability",

abstract = "Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra TΣ/E when the theory (Σ,E) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation of variant satisfiability checking using these sub-algorithms in Maude 2.7.1.",

keywords = "Finite variant property (FVP), Folding variant narrowing, Maude, Metalevel algorithms, Reflection, Satisfiability in initial algebras",

author = "Stephen Skeirik and Jos{\'e} Meseguer",

note = "Funding Information: Partially supported by NSF Grant CNS 13-19109 and by NRL under contract number N00173-17-1-G002 . Publisher Copyright: {\textcopyright} 2018 Elsevier Inc.",

year = "2018",

month = apr,

doi = "10.1016/j.jlamp.2017.12.006",

language = "English (US)",

volume = "96",

pages = "81--110",

journal = "Journal of Logical and Algebraic Methods in Programming",

issn = "2352-2208",

publisher = "Elsevier BV",

}

TY - JOUR

T1 - Metalevel algorithms for variant satisfiability

AU - Skeirik, Stephen

AU - Meseguer, José

PY - 2018/4

Y1 - 2018/4

N2 - Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra TΣ/E when the theory (Σ,E) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation of variant satisfiability checking using these sub-algorithms in Maude 2.7.1.

AB - Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra TΣ/E when the theory (Σ,E) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation of variant satisfiability checking using these sub-algorithms in Maude 2.7.1.

KW - Finite variant property (FVP)

KW - Folding variant narrowing

KW - Maude

KW - Metalevel algorithms

KW - Reflection

KW - Satisfiability in initial algebras

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

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

U2 - 10.1016/j.jlamp.2017.12.006

DO - 10.1016/j.jlamp.2017.12.006

M3 - Article

AN - SCOPUS:85049638989

VL - 96

SP - 81

EP - 110

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

SN - 2352-2208

ER -

Metalevel algorithms for variant satisfiability

Abstract

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this