TY - GEN
T1 - Variant-based decidable satisfiability in initial algebras with predicates
AU - Gutiérrez, Raúl
AU - Meseguer, José
N1 - Funding Information:
Partially supported by NSF Grant CNS 14-09416, NRL under contract number N00173-17-1-G002, the EU (FEDER), Spanish MINECO project TIN2015-69175-C4-1-R and GV project PROMETEOII/2015/013. Raúl Gutiérrez was also supported by INCIBE program “Ayudas para la excelencia de los equipos de investi-gación avanzada en ciberseguridad”.
Publisher Copyright:
© 2018, Springer International Publishing AG, part of Springer Nature.
PY - 2018
Y1 - 2018
N2 - Decision procedures can be either theory-specific, e.g., Presburger arithmetic, or theory-generic, applying to an infinite number of user-definable theories. Variant satisfiability is a theory-generic procedure for quantifier-free satisfiability in the initial algebra of an order-sorted equational theory (Σ, E∪B) under two conditions: (i) E∪B has the finite variant property and B has a finitary unification algorithm; and (ii) (Σ, E∪B) protects a constructor subtheory (Ω,EΩ ∪ B_Ω) that is OS-compact. These conditions apply to many user-definable theories, but have a main limitation: they apply well to data structures, but often do not hold for user-definable predicates on such data structures. We present a theory-generic satisfiability decision procedure, and a prototype implementation, extending variant-based satisfiability to initial algebras with user-definable predicates under fairly general conditions.
AB - Decision procedures can be either theory-specific, e.g., Presburger arithmetic, or theory-generic, applying to an infinite number of user-definable theories. Variant satisfiability is a theory-generic procedure for quantifier-free satisfiability in the initial algebra of an order-sorted equational theory (Σ, E∪B) under two conditions: (i) E∪B has the finite variant property and B has a finitary unification algorithm; and (ii) (Σ, E∪B) protects a constructor subtheory (Ω,EΩ ∪ B_Ω) that is OS-compact. These conditions apply to many user-definable theories, but have a main limitation: they apply well to data structures, but often do not hold for user-definable predicates on such data structures. We present a theory-generic satisfiability decision procedure, and a prototype implementation, extending variant-based satisfiability to initial algebras with user-definable predicates under fairly general conditions.
KW - Decidable validity and satisfiability
KW - Finite variant property (fvp)
KW - OS-compactness
KW - User-definable predicates
KW - in initial algebras
UR - http://www.scopus.com/inward/record.url?scp=85049608702&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85049608702&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-94460-9_18
DO - 10.1007/978-3-319-94460-9_18
M3 - Conference contribution
AN - SCOPUS:85049608702
SN - 9783319944593
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 306
EP - 322
BT - Logic-Based Program Synthesis and Transformation - 27th International Symposium, LOPSTR 2017, Revised Selected Papers
A2 - Fioravanti, Fabio
A2 - Gallagher, John P.
PB - Springer
T2 - 27th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2017
Y2 - 10 October 2017 through 12 October 2017
ER -