{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:26:04Z","timestamp":1725863164213},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319448015"},{"type":"electronic","value":"9783319448022"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-44802-2_10","type":"book-chapter","created":{"date-parts":[[2016,8,17]],"date-time":"2016-08-17T12:32:52Z","timestamp":1471437172000},"page":"167-184","source":"Crossref","is-referenced-by-count":2,"title":["Metalevel Algorithms for Variant Satisfiability"],"prefix":"10.1007","author":[{"given":"Stephen","family":"Skeirik","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":[[2016,8,18]]},"reference":[{"issue":"2","key":"10_CR1","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/3-540-45406-3_3","volume-title":"Constraints in Computational Logics. Theory and Applications","author":"F Baader","year":"2001","unstructured":"Baader, F., Schulz, K.U.: Combining constraint solving. In: Comon, H., March\u00e9, C., Treinen, R. (eds.) CCL 1999. LNCS, vol. 2002, p. 104. Springer, Heidelberg (2001)"},{"key":"10_CR3","first-page":"825","volume-title":"Handbook of Satisfiability","author":"C Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, pp. 825\u2013885. IOS Press, Amsterdam (2009). Chap. 26"},{"key":"10_CR4","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. J. Satisf. Boolean Model. Comput. 3, 21\u201346 (2007)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"10_CR5","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2014","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E., Henzinger, T., Veith, H. (eds.) Handbook of Model Checking. Springer, Berlin (2014)"},{"key":"10_CR6","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, Berlin (2007)"},{"key":"10_CR7","unstructured":"Cholewa, A., Meseguer, J., Escobar, S.: Variants of variants and the finite variant property. Technical report, CS Deptartment, University of Illinois at Urbana-Champaign, February 2014. http:\/\/hdl.handle.net\/2142\/47117"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1684","DOI":"10.1007\/3-540-48118-4_39","volume-title":"FM\u201999 - Formal Methods","author":"M Clavel","year":"1999","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Stehr, M.-O.: Maude as a formal meta-tool. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, p. 1684. Springer, Heidelberg (1999)"},{"key":"10_CR10","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1016\/j.tcs.2006.12.009","volume":"373","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Meseguer, J., Palomino, M.: Reflection in membership equational logic, many-sorted equational logic, horn logic with equality, and rewriting logic. Theoret. Comput. Sci. 373, 70\u201391 (2007)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR11","unstructured":"Comon, H., Dauchet, M., Gilleron, R., L\u00f6ding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007). http:\/\/www.grappa.univ-lille3.fr\/tata . Accessed 12 October 2007"},{"issue":"2","key":"10_CR12","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 118(2), 167\u2013191 (1993)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"10_CR14","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243\u2013320. ACM, North-Holland (1990)"},{"issue":"3","key":"10_CR15","doi-asserted-by":"crossref","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. ACM Trans. Comput. Log. 9(3), 15 (2008)","journal-title":"ACM Trans. Comput. Log."},{"issue":"2\u20133","key":"10_CR16","doi-asserted-by":"crossref","first-page":"201","DOI":"10.3233\/FI-1998-36235","volume":"36","author":"A Dovier","year":"1998","unstructured":"Dovier, A., Policriti, A., Rossi, G.: A uniform axiomatic view of lists, multisets, and sets, and the relevant unification algorithms. Fundam. Inform. 36(2\u20133), 201\u2013234 (1998)","journal-title":"Fundam. Inform."},{"key":"10_CR17","doi-asserted-by":"crossref","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. J. Autom. Reason. 56, 387\u2013457 (2016). https:\/\/hal.archives-ouvertes.fr\/hal-01221066","journal-title":"J. Autom. Reason."},{"key":"10_CR18","doi-asserted-by":"crossref","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Algebr. Log. Program. 81, 898\u2013928 (2012)","journal-title":"J. Algebr. Log. Program."},{"key":"10_CR19","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 105, 217\u2013273 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/978-3-540-32033-3_13","volume-title":"Term Rewriting and Applications","author":"J Hendrix","year":"2005","unstructured":"Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165\u2013174. Springer, Heidelberg (2005)"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/11814771_14","volume-title":"Automated Reasoning","author":"J Hendrix","year":"2006","unstructured":"Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151\u2013155. Springer, Heidelberg (2006)"},{"key":"10_CR22","doi-asserted-by":"crossref","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. SIAM J. Comput. 15, 1155\u20131194 (1986)","journal-title":"SIAM J. Comput."},{"key":"10_CR23","series-title":"Texts in Theoretical Computer Science. An EATCS Series","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 Theoretical Computer Science. An EATCS Series. Springer, Berlin (2008)"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"602","DOI":"10.1007\/978-3-540-71209-1_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 602\u2013617. Springer, Heidelberg (2007)"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376. Springer, Heidelberg (1998)"},{"key":"10_CR26","unstructured":"Meseguer, J.: Strict coherence of conditional rewriting modulo axioms. Technical report, C.S. Department, University of Illinois at Urbana-Champaign, August 2014. http:\/\/hdl.handle.net\/2142\/50288"},{"key":"10_CR27","unstructured":"Meseguer, J.: Variant-based satisfiability in initial algebras. Technical report, University of Illinois at Urbana-Champaign, November 2015. http:\/\/hdl.handle.net\/2142\/88408"},{"key":"10_CR28","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-29510-7_1","volume-title":"Formal Techniques for Safety-Critical Systems","author":"D Mashauri","year":"2016","unstructured":"Mashauri, D., et al.: Variant-based satisfiability in initial algebras. In: Artho, C., et al. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 3\u201334. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-29510-7_1"},{"issue":"1","key":"10_CR29","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1006\/inco.1993.1016","volume":"103","author":"J Meseguer","year":"1993","unstructured":"Meseguer, J., Goguen, J.: Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems. Inf. Comput. 103(1), 114\u2013158 (1993)","journal-title":"Inf. Comput."},{"issue":"2","key":"10_CR30","doi-asserted-by":"crossref","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. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR31","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291\u2013302 (1980)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"594","DOI":"10.1007\/978-3-642-16242-8_42","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Rocha","year":"2010","unstructured":"Rocha, C., Meseguer, J.: Constructors, sufficient completeness, and deadlock freedom of rewrite theories. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 594\u2013609. Springer, Heidelberg (2010)"},{"issue":"1","key":"10_CR33","doi-asserted-by":"crossref","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":"10_CR34","unstructured":"Skeirik, S., Meseguer, J.: Metalevel algorithms for variant satisfiability. Technical report, C.S. Department, University of Illinois at Urbana-Champaign, June 2016. https:\/\/www.ideals.illinois.edu\/handle\/2142\/90238"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-44802-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,6]],"date-time":"2022-07-06T00:08:32Z","timestamp":1657066112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-44802-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319448015","9783319448022"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-44802-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}