Metalevel algorithms for variant satisfiability

Stephen Skeirik; José Meseguer

doi:10.1007/978-3-319-44802-2_10

Metalevel algorithms for variant satisfiability

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

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 in Maude 2.7 of variant satisfiability using these sub-algorithms.

Original language	English (US)
Title of host publication	Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers
Editors	Dorel Lucanu
Publisher	Springer
Pages	167-184
Number of pages	18
ISBN (Print)	9783319448015
DOIs	https://doi.org/10.1007/978-3-319-44802-2_10
State	Published - 2016
Event	11th International Workshop on Rewriting Logic and its Applications, WRLA 2016 held as a Satellite Event of European Joint Conferences on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands Duration: Apr 2 2016 → Apr 3 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9942 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	11th International Workshop on Rewriting Logic and its Applications, WRLA 2016 held as a Satellite Event of European Joint Conferences on Theory and Practice of Software, ETAPS 2016
Country/Territory	Netherlands
City	Eindhoven
Period	4/2/16 → 4/3/16

Keywords

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

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-319-44802-2_10

Library availability

Discover UIUC Full Text

Cite this

Skeirik, S., & Meseguer, J. (2016). Metalevel algorithms for variant satisfiability. In D. Lucanu (Ed.), Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers (pp. 167-184). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9942 LNCS). Springer. https://doi.org/10.1007/978-3-319-44802-2_10

Metalevel algorithms for variant satisfiability. / Skeirik, Stephen; Meseguer, José.
Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. ed. / Dorel Lucanu. Springer, 2016. p. 167-184 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9942 LNCS).

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

Skeirik, S & Meseguer, J 2016, Metalevel algorithms for variant satisfiability. in D Lucanu (ed.), Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9942 LNCS, Springer, pp. 167-184, 11th International Workshop on Rewriting Logic and its Applications, WRLA 2016 held as a Satellite Event of European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, Netherlands, 4/2/16. https://doi.org/10.1007/978-3-319-44802-2_10

Skeirik S, Meseguer J. Metalevel algorithms for variant satisfiability. In Lucanu D, editor, Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. Springer. 2016. p. 167-184. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-44802-2_10

Skeirik, Stephen ; Meseguer, José. / Metalevel algorithms for variant satisfiability. Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers. editor / Dorel Lucanu. Springer, 2016. pp. 167-184 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{04a80ceb030e445480eceaff690e3514,

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 in Maude 2.7 of variant satisfiability using these sub-algorithms.",

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

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

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016.; 11th International Workshop on Rewriting Logic and its Applications, WRLA 2016 held as a Satellite Event of European Joint Conferences on Theory and Practice of Software, ETAPS 2016 ; Conference date: 02-04-2016 Through 03-04-2016",

year = "2016",

doi = "10.1007/978-3-319-44802-2_10",

language = "English (US)",

isbn = "9783319448015",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "167--184",

editor = "Dorel Lucanu",

booktitle = "Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers",

address = "Germany",

}

TY - GEN

T1 - Metalevel algorithms for variant satisfiability

AU - Skeirik, Stephen

AU - Meseguer, José

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2016.

PY - 2016

Y1 - 2016

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 in Maude 2.7 of variant satisfiability using these sub-algorithms.

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 in Maude 2.7 of variant satisfiability using these sub-algorithms.

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=84986220614&partnerID=8YFLogxK

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

U2 - 10.1007/978-3-319-44802-2_10

DO - 10.1007/978-3-319-44802-2_10

M3 - Conference contribution

AN - SCOPUS:84986220614

SN - 9783319448015

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 167

EP - 184

BT - Rewriting Logic and Its Applications - 11th International Workshop, WRLA 2016 Held as a Satellite Event of ETAPS 2016, Revised Selected Papers

A2 - Lucanu, Dorel

PB - Springer

T2 - 11th International Workshop on Rewriting Logic and its Applications, WRLA 2016 held as a Satellite Event of European Joint Conferences on Theory and Practice of Software, ETAPS 2016

Y2 - 2 April 2016 through 3 April 2016

ER -

Metalevel algorithms for variant satisfiability

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this