{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:17:21Z","timestamp":1784837841689,"version":"3.55.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T00:00:00Z","timestamp":1748304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T00:00:00Z","timestamp":1748304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100007052","name":"Universit\u00e0 degli Studi di Verona","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007052","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Deciding the satisfiability of formulas involving both quantifiers and theory defined symbols is a challenge in automated reasoning. This article presents an algorithm, called <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{QSMA}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>QSMA<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> (<jats:italic>Quantified Satisfiability Modulo Assignment<\/jats:italic>), for the satisfiability of an arbitrary quantified formula modulo a complete theory and an initial assignment. The algorithm is proved partially correct and terminating, so that its total correctness is established. An optimized variant called <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{OptiQSMA}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>OptiQSMA<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> is also described and shown to preserve both partial correctness and termination. <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{OptiQSMA}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>OptiQSMA<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> is implemented in the YicesQS solver. <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{OptiQSMA}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>OptiQSMA<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> enabled YicesQS to achieve top of the line results, especially in linear rational arithmetic, in the 2022, 2023, and 2024 editions of the International Satisfiability Modulo Theories Competition (SMT-COMP). A report on these results in four fragments of arithmetic (<jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{LRA}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>LRA<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\u2014Linear Rational Arithmetic, <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{LIA}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>LIA<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\u2014Linear Integer Arithmetic, <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{NRA}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>NRA<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\u2014Nonlinear Real Arithmetic, and <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{NIA}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>NIA<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\u2014Nonlinear Integer Arithmetic) and in the theory of bitvectors (<jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf{BV}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>BV<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>) is included.<\/jats:p>","DOI":"10.1007\/s10817-025-09727-8","type":"journal-article","created":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T19:31:11Z","timestamp":1748374271000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["The QSMA Algorithm for Quantifiers in SMT"],"prefix":"10.1007","volume":"69","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"St\u00e9phane","family":"Graham-Lengrand","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christophe","family":"Vauthier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,27]]},"reference":[{"key":"9727_CR1","doi-asserted-by":"publisher","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) Proc. FroCoS-7. LNAI, vol. 5749, pp. 84\u201399. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_5","DOI":"10.1007\/978-3-642-04222-5_5"},{"key":"9727_CR2","doi-asserted-by":"publisher","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) Proc. CADE-24. LNAI, vol. 7898, pp. 39\u201357. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_3","DOI":"10.1007\/978-3-642-38574-2_3"},{"key":"9727_CR3","series-title":"EPiC Series in Computing","first-page":"15","volume-title":"Short Presentations at LPAR-20","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Janota, M.: Playing with quantified satisfaction (Short paper). In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A. (eds.) Short Presentations at LPAR-20. EPiC Series in Computing, vol. 35, pp. 15\u201327. EasyChair, Manchester (2015)"},{"key":"9727_CR4","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P.: Reasoning about quantifiers in SMT: the QSMA algorithm (Abstract). In: Nadel, A., Rozier, K.Y. (eds.) Proc. FMCAD-23, pp. 1\u20131. TU Wien Academic Press, Vienna (2023). https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_1","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_1"},{"issue":"2","key":"9727_CR5","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/s10817-016-9384-2","volume":"59","author":"MP Bonacina","year":"2017","unstructured":"Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: inference system and completeness. J. Autom. Reason. 59(2), 165\u2013218 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9384-2","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9727_CR6","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/s10817-018-09510-y","volume":"64","author":"MP Bonacina","year":"2020","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Conflict-driven satisfiability for theory combination: transition system and completeness. J. Autom. Reason. 64(3), 579\u2013609 (2020). https:\/\/doi.org\/10.1007\/s10817-018-09510-y","journal-title":"J. Autom. Reason."},{"key":"9727_CR7","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: CDSAT for nondisjoint theories with shared predicates: arrays with abstract length. In: Hyv\u00e4rinen, A., D\u00e9harbe, D. (eds.) Proc. SMT-20. CEUR Proceedings, vol. 3185, pp. 18\u201337. CEUR WS-org, Aachen (2022). https:\/\/ceur-ws.org\/Vol-3185\/"},{"issue":"1","key":"9727_CR8","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s10817-021-09606-y","volume":"66","author":"MP Bonacina","year":"2022","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs. J. Autom. Reason. 66(1), 43\u201391 (2022). https:\/\/doi.org\/10.1007\/s10817-021-09606-y","journal-title":"J. Autom. Reason."},{"key":"9727_CR9","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Vauthier, C.: QSMA: a new algorithm for quantified satisfiability modulo theory and assignment. In: Pientka, B., Tinelli, C. (eds.) Proc. CADE-29. LNAI, vol. 14132, pp. 78\u201395. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_5","DOI":"10.1007\/978-3-031-38499-8_5"},{"key":"9727_CR10","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161\u2013189 (2011). https:\/\/doi.org\/10.1007\/s10817-010-9213-y","DOI":"10.1007\/s10817-010-9213-y"},{"key":"9727_CR11","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation\u2014Decision Procedures with Applications to Verification. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-74113-8","DOI":"10.1007\/978-3-540-74113-8"},{"key":"9727_CR12","doi-asserted-by":"publisher","unstructured":"Caviness, B.F., Johnson, J.R.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Wien (1998). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1","DOI":"10.1007\/978-3-7091-9459-1"},{"key":"9727_CR13","doi-asserted-by":"publisher","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Proc. 2nd GI Conf. on Automata Theory and Formal Languages. LNCS, vol. 33, pp. 134\u2013183. Springer, Heidelberg (1975). https:\/\/doi.org\/10.1007\/3-540-07407-4_17","DOI":"10.1007\/3-540-07407-4_17"},{"key":"9727_CR14","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT-solvers. In: Pfenning, F. (ed.) Proc. CADE-21. LNAI, vol. 4603, pp. 183\u2013198. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"9727_CR15","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Bugs, moles, and skeletons: symbolic reasoning for software development. In: Giesl, J., H\u00e4hnle, R. (eds.) Proc. IJCAR-5. LNAI, vol. 6173, pp. 400\u2013411. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_34","DOI":"10.1007\/978-3-642-14203-1_34"},{"key":"9727_CR16","doi-asserted-by":"publisher","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Proc. VMCAI-14. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1","DOI":"10.1007\/978-3-642-35873-9_1"},{"issue":"3","key":"9727_CR17","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"DL Detlefs","year":"2005","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005). https:\/\/doi.org\/10.1145\/1066100.1066102","journal-title":"J. ACM"},{"key":"9727_CR18","unstructured":"Dutertre, B.: Solving exists\/forall problems with Yices (2015). https:\/\/brunodutertre.github.io\/"},{"key":"9727_CR19","doi-asserted-by":"publisher","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiability modulo theories. In: Bouajjani, A., Maler, O. (eds.) Proc. CAV-21. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"9727_CR20","doi-asserted-by":"publisher","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) Proc. CADE-21. LNAI, vol. 4603, pp. 167\u2013182. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_12","DOI":"10.1007\/978-3-540-73595-3_12"},{"key":"9727_CR21","doi-asserted-by":"publisher","unstructured":"Graham-Lengrand, S., Jovanovi\u0107, D., Dutertre, B.: Solving bitvectors with MCSAT: explanations from bits and pieces. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Proc. IJCAR-10. LNAI, vol. 12166, pp. 103\u2013121. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_7","DOI":"10.1007\/978-3-030-51074-9_7"},{"key":"9727_CR22","doi-asserted-by":"publisher","unstructured":"Janota, M., Barbosa, H., Fontaine, P., Reynolds, A.: Fair and adventurous enumeration of quantifier instantiations. In: Piskac, R., Whalen, M.W. (eds.) Proc. FMCAD-21, pp. 256\u2013260. TU Wien Academic Press, Vienna (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_35","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_35"},{"key":"9727_CR23","doi-asserted-by":"publisher","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Proc. IJCAR-6. LNAI, vol. 7364, pp. 339\u2013354. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"9727_CR24","doi-asserted-by":"publisher","unstructured":"Jovanovi\u0107, D., Dutertre, B.: Interpolation and model checking for nonlinear arithmetic. In: Silva, A., Leino, K.R.M. (eds.) Proc. CAV-35. LNCS, vol. 12760, pp. 266\u2013288. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_13","DOI":"10.1007\/978-3-030-81688-9_13"},{"key":"9727_CR25","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) Proc. CAV-26. LNCS, vol. 8559, pp. 17\u201334. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2","DOI":"10.1007\/978-3-319-08867-9_2"},{"issue":"3","key":"9727_CR26","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Form. Methods Syst. Des. 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Form. Methods Syst. Des."},{"key":"9727_CR27","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: Kaivola, R., Wahl, T. (eds.) Proc. FMCAD 2015, pp. 89\u201396. FMCAD Inc., Austin (2015). https:\/\/doi.org\/10.5555\/2893529.2893548","DOI":"10.5555\/2893529.2893548"},{"key":"9727_CR28","doi-asserted-by":"publisher","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) Proc. CSL-16. LNCS, vol. 4646, pp. 223\u2013237. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_19","DOI":"10.1007\/978-3-540-74915-8_19"},{"key":"9727_CR29","series-title":"Texts in Theoretical Computer Science","volume-title":"Decision Procedures\u2014An Algorithmic Point of View","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures\u2014An Algorithmic Point of View. Texts in Theoretical Computer Science, Springer, Berlin (2008)"},{"key":"9727_CR30","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/BF00245296","volume":"9","author":"J-L Lassez","year":"1992","unstructured":"Lassez, J.-L., Maher, M.J.: On Fourier\u2019s algorithm for linear arithmetic constraints. J. Autom. Reason. 9, 373\u2013379 (1992). https:\/\/doi.org\/10.1007\/BF00245296","journal-title":"J. Autom. Reason."},{"issue":"5","key":"9727_CR31","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450\u2013462 (1993). https:\/\/doi.org\/10.1093\/comjnl\/36.5.450","journal-title":"Comput. J."},{"key":"9727_CR32","doi-asserted-by":"publisher","unstructured":"Lopez Hernandez, J., Korovin, K.: An abstraction refinement framework for reasoning with large theories. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Proc. IJCAR-9. LNAI, vol. 10900, pp. 663\u2013679. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_43","DOI":"10.1007\/978-3-319-94205-6_43"},{"key":"9727_CR33","unstructured":"Moskal, M.: Fx7 or in software, it is all about quantifiers. System Descriptions at SMT-COMP (2007). http:\/\/smtcomp.cs.uiowa.edu\/2007\/descriptions\/fx7.pdf"},{"key":"9727_CR34","doi-asserted-by":"publisher","unstructured":"Nalbach, J., Promies, V., \u00c1brah\u00e1m, E., Kobialka, P.: FMplex: A novel method for solving linear real arithmetic problems. In: Achilleos, A., Monica, D.D. (eds.) Proc. GandALF-14. EPTCS, vol. 390, pp. 16\u201332 (2023). https:\/\/doi.org\/10.4204\/EPTCS.390.2","DOI":"10.4204\/EPTCS.390.2"},{"key":"9727_CR35","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Solving quantified bit-vectors using invertibility conditions. In: Chockler, H., Weissenbacher, G. (eds.) Proc. CAV-30. LNCS, vol. 10982, pp. 236\u2013255. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_16","DOI":"10.1007\/978-3-319-96142-2_16"},{"key":"9727_CR36","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Syntax-guided quantifier instantiation. In: Groote, J., Larsen, K. (eds.) Proc. TACAS-27. LNCS, vol. 12652, pp. 145\u2013163. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_8","DOI":"10.1007\/978-3-030-72013-1_8"},{"issue":"2","key":"9727_CR37","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10817-010-9183-0","volume":"45","author":"T Nipkow","year":"2010","unstructured":"Nipkow, T.: Linear quantifier elimination. J. Autom. Reason. 45(2), 189\u2013212 (2010). https:\/\/doi.org\/10.1007\/s10817-010-9183-0","journal-title":"J. Autom. Reason."},{"key":"9727_CR38","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D., Huisman, M. (eds.) Proc. TACAS-24. LNCS, vol. 10806, pp. 112\u2013131. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_7","DOI":"10.1007\/978-3-319-89963-3_7"},{"key":"9727_CR39","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/s10703-017-0290-y","volume":"51","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving quantified linear arithmetic by counterexample-guided instantiation. Form. Methods Syst. Des. 51, 500\u2013532 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0290-y","journal-title":"Form. Methods Syst. Des."},{"key":"9727_CR40","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: Claessen, K., Kuncak, V. (eds.) Proc. FMCAD 2014, pp. 195\u2013202. FMCAD Inc., Austin (2014). https:\/\/doi.org\/10.5555\/2682923.2682957","DOI":"10.5555\/2682923.2682957"},{"key":"9727_CR41","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) Proc. CADE-24. LNAI, vol. 7898, pp. 377\u2013391. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_26","DOI":"10.1007\/978-3-642-38574-2_26"},{"issue":"1\u20132","key":"9727_CR42","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput. 5(1\u20132), 2\u201327 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80003-8","journal-title":"J. Symb. Comput."},{"issue":"2","key":"9727_CR43","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra\u2014the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85\u2013101 (1997). https:\/\/doi.org\/10.1007\/s002000050055","journal-title":"Appl. Algebra Eng. Commun. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09727-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09727-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09727-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T09:04:15Z","timestamp":1750669455000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09727-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,27]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["9727"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09727-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,27]]},"assertion":[{"value":"13 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 April 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"13"}}