TY - JOUR
T1 - Variant-based satisfiability in initial algebras
AU - Meseguer, José
N1 - Funding Information:
I thank the organizers of FTSCS 2015 for inviting me to present these ideas in Paris, and the FTSCS participants for their interest and very helpful comments. I thank the anonymous referees for their careful and constructive criticism and their very helpful suggestions that have resulted in a substantially improved final version. I thank Andrew Cholewa, Steven Eker, Santiago Escobar, Ralf Sasse, and Carolyn Talcott for their contributions to the development of the theory and Maude implementation of folding variant narrowing, and Stephen Skeirik and Raúl Gutiérrez for their help in advancing the algorithms and implementations for variant-based satisfiability. I have learned much about satisfiability from Maria-Paola Bonacina, Vijay Ganesh and Cesare Tinelli along many conversations; I am most grateful to them for their kind enlightenment. I also thank the following persons for their very helpful comments on earlier drafts: Maria-Paola Bonacina, Santiago Escobar, Dorel Lucanu, Peter Ölveczky, Vlad Rusu, Ralf Sasse, Natarajan Shankar, and Cesare Tinelli. The pioneering work of Hubert Comon-Lundh about compact theories [30] , and that of him with Stéphanie Delaune about the finite variant property [32] , have both been important sources of inspiration for the ideas presented here. This work has been partially supported by NSF Grant CNS 13-19109 .
Publisher Copyright:
© 2017
PY - 2018/3/1
Y1 - 2018/3/1
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 one needs theory-generic satisfiability algorithms allowing a potentially infinite number of decidable theories to be user-definable, instead of needing to be built in by tool implementers. 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 user-specified input theories when such theories satisfy Comon and 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 illustrated with examples. A method based on descent maps to bring other theories into these classes and to improve the generic algorithm's efficiency is also proposed.
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 one needs theory-generic satisfiability algorithms allowing a potentially infinite number of decidable theories to be user-definable, instead of needing to be built in by tool implementers. 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 user-specified input theories when such theories satisfy Comon and 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 illustrated with examples. A method based on descent maps to bring other theories into these classes and to improve the generic algorithm's efficiency is also proposed.
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=85034809827&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85034809827&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2017.09.001
DO - 10.1016/j.scico.2017.09.001
M3 - Article
AN - SCOPUS:85034809827
SN - 0167-6423
VL - 154
SP - 3
EP - 41
JO - Science of Computer Programming
JF - Science of Computer Programming
ER -