{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T06:50:02Z","timestamp":1778914202601,"version":"3.51.4"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319944593","type":"print"},{"value":"9783319944609","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94460-9_18","type":"book-chapter","created":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T11:36:38Z","timestamp":1531136198000},"page":"306-322","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Variant-Based Decidable Satisfiability in Initial Algebras with Predicates"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3984-2868","authenticated-orcid":false,"given":"Ra\u00fal","family":"Guti\u00e9rrez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,10]]},"reference":[{"issue":"1","key":"18_CR1","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/1459010.1459014","volume":"10","author":"A Armando","year":"2009","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. TOCL 10(1), 4 (2009)","journal-title":"TOCL"},{"issue":"2","key":"18_CR2","first-page":"140","volume":"183","author":"A Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. I&C 183(2), 140\u2013164 (2003)","journal-title":"I&C"},{"key":"18_CR3","first-page":"21","volume":"3","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of inductive data types. JSAT 3, 21\u201346 (2007)","journal-title":"JSAT"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-40885-4_23","volume-title":"Frontiers of Combining Systems","author":"C Bouchard","year":"2013","unstructured":"Bouchard, C., Gero, K.A., Lynch, C., Narendran, P.: On forward closure and the finite variant property. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 327\u2013342. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-40885-4_23"},{"key":"18_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8","volume-title":"The Calculus of Computation - Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation - Decision Procedures with Applications to Verification. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74113-8"},{"key":"18_CR6","unstructured":"Cholewa, A., Meseguer, J., Escobar, S.: Variants of variants and the finite variant property. Technical report, CS Dept. University of Illinois at Urbana-Champaign (2014). \nhttp:\/\/hdl.handle.net\/2142\/47117"},{"key":"18_CR7","unstructured":"Ciobaca., S.: Verification of composition of security protocols with applications to electronic voting. Ph.D. thesis, ENS Cachan (2011)"},{"issue":"2","key":"18_CR8","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0304-3975(93)90108-6","volume":"118","author":"H Comon","year":"1993","unstructured":"Comon, H.: Complete axiomatizations of some quotient term algebras. TCS 118(2), 167\u2013191 (1993)","journal-title":"TCS"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-32033-3_22"},{"key":"18_CR10","first-page":"243","volume-title":"Formal Models and Semantics","author":"Nachum DERSHOWITZ","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: Handbook of Theoretical Computer Science, North-Holland, vol. B, pp. 243\u2013320 (1990)"},{"issue":"3","key":"18_CR11","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/1352582.1352583","volume":"9","author":"A Dovier","year":"2008","unstructured":"Dovier, A., Piazza, C., Rossi, G.: A uniform approach to constraint-solving for lists, multisets, compact lists, and sets. TOCL 9(3), 15 (2008)","journal-title":"TOCL"},{"issue":"4","key":"18_CR12","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/s10817-015-9352-2","volume":"56","author":"C Dross","year":"2016","unstructured":"Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Adding decision procedures to SMT solvers using axioms with triggers. JAR 56(4), 387\u2013457 (2016)","journal-title":"JAR"},{"key":"18_CR13","first-page":"898","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. JALP 81, 898\u2013928 (2012)","journal-title":"JALP"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0014969","volume-title":"TAPSOFT 1987","author":"JA Goguen","year":"1987","unstructured":"Goguen, J.A., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT 1987. LNCS, vol. 250, pp. 1\u201322. Springer, Heidelberg (1987). \nhttps:\/\/doi.org\/10.1007\/BFb0014969"},{"key":"18_CR15","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J Goguen","year":"1992","unstructured":"Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. TCS 105, 217\u2013273 (1992)","journal-title":"TCS"},{"key":"18_CR16","unstructured":"Guti\u00e9rrez, R., Meseguer, J.: Variant satisfiability in initial algebras with predicates. Technical report, CS Department, University of Illinois at Urbana-Champaign (2018). \nhttp:\/\/hdl.handle.net\/2142\/99039"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"JP Jouannaud","year":"1986","unstructured":"Jouannaud, J.P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SICOMP 15, 1155\u20131194 (1986)","journal-title":"SICOMP"},{"key":"18_CR18","series-title":"Texts in TCS. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3","volume-title":"Decision Procedures - An algorithmic point of view","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An algorithmic point of view. Texts in TCS. An EATCS Series. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74105-3"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Lynch, C., Morawska, B.: Automatic decidability. In: Proceedings of LICS 2002, p. 7. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029813"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-73595-3_22","volume-title":"Automated Deduction \u2013 CADE-21","author":"C Lynch","year":"2007","unstructured":"Lynch, C., Tran, D.-K.: Automatic decidability and combinability revisited. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 328\u2013344. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-73595-3_22"},{"key":"18_CR21","first-page":"3","volume":"154","author":"J Meseguer","year":"2018","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. SCP 154, 3\u201341 (2018)","journal-title":"SCP"},{"key":"18_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2016.12.026","volume":"672","author":"J Meseguer","year":"2017","unstructured":"Meseguer, J.: Strict coherence of conditional rewriting modulo axioms. TCS 672, 1\u201335 (2017)","journal-title":"TCS"},{"key":"18_CR23","unstructured":"Meseguer, J., Goguen, J.: Initiality, induction and computability. In: Algebraic Methods in Semantics, Cambridge, pp. 459\u2013541 (1985)"},{"issue":"1","key":"18_CR24","first-page":"114","volume":"103","author":"J Meseguer","year":"1993","unstructured":"Meseguer, J., Goguen, J.: Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems. I&C 103(1), 114\u2013158 (1993)","journal-title":"I&C"},{"issue":"2","key":"18_CR25","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS 1(2), 245\u2013257 (1979)","journal-title":"TOPLAS"},{"issue":"1","key":"18_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"RE Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1\u201312 (1984)","journal-title":"J. ACM"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-44802-2_10","volume-title":"Rewriting Logic and Its Applications","author":"S Skeirik","year":"2016","unstructured":"Skeirik, S., Meseguer, J.: Metalevel algorithms for variant satisfiability. In: Lucanu, D. (ed.) WRLA 2016. LNCS, vol. 9942, pp. 167\u2013184. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-44802-2_10"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: Proceedings of LICS 2001, pp. 29\u201337. IEEE (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"18_CR29","first-page":"3","volume":"99","author":"E Tushkanova","year":"2015","unstructured":"Tushkanova, E., Giorgetti, A., Ringeissen, C., Kouchnarenko, O.: A rule-based system for automatic decidability and combinability. SCP 99, 3\u201323 (2015)","journal-title":"SCP"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94460-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T11:46:11Z","timestamp":1531136771000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94460-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319944593","9783319944609"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94460-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}