{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T02:13:44Z","timestamp":1783649624867,"version":"3.55.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"Abstract<\/jats:title>\n \n Automated reasoning is routinely used in the rigorous construction and analysis of complex systems. Among different theories, arithmetic stands out as one of the most frequently used and at the same time one of the most challenging in the presence of quantifiers and uninterpreted function symbols. First-order theorem provers perform very well on quantified problems due to the efficient superposition calculus, but support for arithmetic reasoning is limited to heuristic axioms. In this paper, we introduce the\n \n \n $$\\textsc {Alasca}$$<\/jats:tex-math>\n \n \n A<\/mml:mi>\n \n L<\/mml:mi>\n A<\/mml:mi>\n S<\/mml:mi>\n C<\/mml:mi>\n A<\/mml:mi>\n <\/mml:mstyle>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n calculus that lifts superposition reasoning to the linear arithmetic domain. We show that\n \n \n $$\\textsc {Alasca}$$<\/jats:tex-math>\n \n \n A<\/mml:mi>\n \n L<\/mml:mi>\n A<\/mml:mi>\n S<\/mml:mi>\n C<\/mml:mi>\n A<\/mml:mi>\n <\/mml:mstyle>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n is both sound and complete with respect to an axiomatisation of linear arithmetic. We implemented and evaluated\n \n \n $$\\textsc {Alasca}$$<\/jats:tex-math>\n \n \n A<\/mml:mi>\n \n L<\/mml:mi>\n A<\/mml:mi>\n S<\/mml:mi>\n C<\/mml:mi>\n A<\/mml:mi>\n <\/mml:mstyle>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n using the\n Vampire<\/jats:sc>\n theorem prover, solving many more challenging problems compared to state-of-the-art reasoners.\n <\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_33","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"647-665","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["ALASCA: Reasoning in Quantified Linear Arithmetic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0740-621X","authenticated-orcid":false,"given":"Konstantin","family":"Korovin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Giles","family":"Reger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5550-196X","authenticated-orcid":false,"given":"Johannes","family":"Schoisswohl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"33_CR1","doi-asserted-by":"publisher","unstructured":"Alt, L., Blicha, M., Hyv\u00e4rinen, A.E.J., Sharygina, N.: SolCMC: Solidity Compiler\u2019s Model Checker. In: CAV, LNCS, vol. 13371, pp. 325\u2013338, Springer (2022), https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16","DOI":"10.1007\/978-3-031-13185-1_16"},{"key":"33_CR2","unstructured":"Andreotti, B., Barbosa, H., Fontaine, P., Schurr, H.J.: veriT at SMT-COMP 2022. https:\/\/smt-comp.github.io\/2022\/system-descriptions\/veriT.pdf (2022)"},{"key":"33_CR3","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Ordered Chaining Calculi for First-Order Theories of Transitive Relations. J. ACM 45(6), 1007\u20131049 (1998), https:\/\/doi.org\/10.1145\/293347.293352, https:\/\/doi.org\/10.1145\/293347.293352","DOI":"10.1145\/293347.293352"},{"key":"33_CR4","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Resolution Theorem Proving. In: Handbook of Automated Reasoning, pp. 19\u201399, Elsevier and MIT Press (2001), https:\/\/doi.org\/10.1016\/b978-044450813-3\/50004-7","DOI":"10.1016\/b978-044450813-3\/50004-7"},{"key":"33_CR5","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., , Zohar, Y.: CVC5 at the SMT Competition 2022. https:\/\/smt-comp.github.io\/2022\/system-descriptions\/cvc5.pdf (2022)"},{"key":"33_CR6","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A Versatile and Industrial-Strength SMT Solver. In: TACAS, LNCS, vol. 13243, pp. 415\u2013442, Springer (2022), https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"33_CR7","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"33_CR8","unstructured":"Barth, M., Dietsch, D., Heizmann, M., Podelski, A.: Ultimate Eliminator at SMT-COMP 2022. https:\/\/smt-comp.github.io\/2022\/system-descriptions\/UltimateEliminator%2BMathSAT.pdf (2022)"},{"key":"33_CR9","doi-asserted-by":"publisher","unstructured":"Baumgartner, P., Bax, J., Waldmann, U.: Beagle - A Hierarchic Superposition Theorem Prover. In: CADE, LNCS, vol. 9195, pp. 367\u2013377, Springer (2015), https:\/\/doi.org\/10.1007\/978-3-319-21401-6_25","DOI":"10.1007\/978-3-319-21401-6_25"},{"key":"33_CR10","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Satisfiability Modulo Theories and Assignments. In: CADE, LNCS, vol. 10395, pp. 42\u201359, Springer (2017), https:\/\/doi.org\/10.1007\/978-3-319-63046-5_4","DOI":"10.1007\/978-3-319-63046-5_4"},{"key":"33_CR11","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Fleury, M., Schwarz, S., Weidenbach, C.: SPASS-SATT - A CDCL(LA) solver. In: CADE, LNCS, vol. 11716, pp. 111\u2013122, Springer (2019), https:\/\/doi.org\/10.1007\/978-3-030-29436-6_7","DOI":"10.1007\/978-3-030-29436-6_7"},{"key":"33_CR12","doi-asserted-by":"publisher","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: TACAS, LNCS, vol. 6015, pp. 150\u2013153, Springer (2010), https:\/\/doi.org\/10.1007\/978-3-642-12002-2_12","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"33_CR13","doi-asserted-by":"publisher","unstructured":"Cook, B.: Formal Reasoning About the Security of Amazon Web Services. In: CAV, LNCS, vol. 10981, pp. 38\u201347, Springer (2018), https:\/\/doi.org\/10.1007\/978-3-319-96145-3_3","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"33_CR14","unstructured":"Cruanes, S.: Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond. Ph.D. thesis, Ecole Polytechnique, Paris, France (2015)"},{"key":"33_CR15","doi-asserted-by":"publisher","unstructured":"Desharnais, M., Vukmirovic, P., Blanchette, J., Wenzel, M.: Seventeen Provers Under the Hammer. In: ITP, LIPIcs, vol. 237, pp. 8:1\u20138:18 (2022), https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.8","DOI":"10.4230\/LIPIcs.ITP.2022.8"},{"key":"33_CR16","doi-asserted-by":"publisher","unstructured":"Distefano, D., F\u00e4hndrich, M., Logozzo, F., O\u2019Hearn, P.W.: Scaling Static Analyses at Facebook. Commun. ACM 62(8), 62\u201370 (2019), https:\/\/doi.org\/10.1145\/3338112","DOI":"10.1145\/3338112"},{"key":"33_CR17","doi-asserted-by":"publisher","unstructured":"Duarte, A., Korovin, K.: Implementing Superposition in iProver (System Description). In: IJCAR, LNCS, vol. 12167, pp. 388\u2013397, Springer (2020), https:\/\/doi.org\/10.1007\/978-3-030-51054-1_24","DOI":"10.1007\/978-3-030-51054-1_24"},{"key":"33_CR18","doi-asserted-by":"publisher","unstructured":"Elad, N., Rain, S., Immerman, N., Kov\u00e1cs, L., Sagiv, M.: Summing up Smart Transitions. In: CAV, LNCS, vol. 12759, pp. 317\u2013340, Springer (2021), https:\/\/doi.org\/10.1007\/978-3-030-81685-8_15","DOI":"10.1007\/978-3-030-81685-8_15"},{"key":"33_CR19","unstructured":"Graham-Lengrand, S.: Yices-QS 2022, an extension of Yices for quantified satisfiability. https:\/\/smt-comp.github.io\/2022\/system-descriptions\/YicesQS.pdf (2022)"},{"key":"33_CR20","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A.: Program Verification with Constrained Horn Clauses (Invited Paper). In: CAV, LNCS, vol. 13371, pp. 19\u201329, Springer (2022), https:\/\/doi.org\/10.1007\/978-3-031-13185-1_2","DOI":"10.1007\/978-3-031-13185-1_2"},{"key":"33_CR21","unstructured":"Hoenicke, J., Schindler, T.: SMTInterpol with Resolution Proofs. https:\/\/smt-comp.github.io\/2022\/system-descriptions\/smtinterpol.pdf (2022)"},{"key":"33_CR22","doi-asserted-by":"publisher","unstructured":"Kapur, D., Narendran, P.: Double-exponential Complexity of Computing a Complete Set of AC-Unifiers. In: LICS, pp. 11\u201321, IEEE Computer Society (1992), https:\/\/doi.org\/10.1109\/LICS.1992.185515","DOI":"10.1109\/LICS.1992.185515"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Korovin, K., Kov\u00e1cs, L., Schoisswohl, J., Reger, G., Voronkov, A.: ALASCA:Reasoning in Quantified Linear Arithmetic (Extended Version). EasyChair Preprint no. 9606 (2023)","DOI":"10.1007\/978-3-031-30823-9_33"},{"key":"33_CR24","doi-asserted-by":"publisher","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict Resolution. In: CP, LNCS, vol. 5732, pp. 509\u2013523, Springer (2009), https:\/\/doi.org\/10.1007\/978-3-642-04244-7_41","DOI":"10.1007\/978-3-642-04244-7_41"},{"key":"33_CR25","doi-asserted-by":"publisher","unstructured":"Korovin, K., Voronkov, A.: An AC-Compatible Knuth-Bendix Order. In: CADE, LNCS, vol. 2741, pp. 47\u201359, Springer (2003), https:\/\/doi.org\/10.1007\/978-3-540-45085-6_5","DOI":"10.1007\/978-3-540-45085-6_5"},{"key":"33_CR26","doi-asserted-by":"publisher","unstructured":"Korovin, K., Voronkov, A.: Integrating Linear Arithmetic into Superposition Calculus. In: CSLs, LNCS, vol. 4646, pp. 223\u2013237, Springer (2007), https:\/\/doi.org\/10.1007\/978-3-540-74915-8_19","DOI":"10.1007\/978-3-540-74915-8_19"},{"key":"33_CR27","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In: CAV, LNCS, vol. 8044, pp. 1\u201335, Springer (2013), https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"33_CR28","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Efficient E-Matching for SMT Solvers. In: CADE, LNCS, vol. 4603, pp. 183\u2013198, Springer (2007), https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"33_CR29","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: TACAS, LNCS, vol. 4963, pp. 337\u2013340, Springer (2008), https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"33_CR30","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Jovanovic, D.: A Model-Constructing Satisfiability Calculus. In: VMCAI, LNCS, vol. 7737, pp. 1\u201312, Springer (2013), https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1","DOI":"10.1007\/978-3-642-35873-9_1"},{"key":"33_CR31","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Handbook of Automated Reasoning, pp. 371\u2013443, Elsevier and MIT Press (2001), https:\/\/doi.org\/10.1016\/b978-044450813-3\/50009-6","DOI":"10.1016\/b978-044450813-3\/50009-6"},{"key":"33_CR32","doi-asserted-by":"publisher","unstructured":"Passmore, G.O.: Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms. In: FM, LNCS, vol. 13047, pp. 717\u2013721, Springer (2021), https:\/\/doi.org\/10.1007\/978-3-030-90870-6_39","DOI":"10.1007\/978-3-030-90870-6_39"},{"key":"33_CR33","doi-asserted-by":"publisher","unstructured":"Reger, G., Bj\u00f8rner, N.S., Suda, M., Voronkov, A.: AVATAR Modulo Theories. In: GCAI, EPiC Series in Computing, vol.\u00a041, pp. 39\u201352, EasyChair (2016), https:\/\/doi.org\/10.29007\/k6tp","DOI":"10.29007\/k6tp"},{"key":"33_CR34","doi-asserted-by":"publisher","unstructured":"Reger, G., Suda, M., Voronkov, A.: Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. In: TACAS, LNCS, vol. 10805, pp. 3\u201322, Springer (2018), https:\/\/doi.org\/10.1007\/978-3-319-89960-2_1","DOI":"10.1007\/978-3-319-89960-2_1"},{"key":"33_CR35","unstructured":"Reger, G., Suda, M., Voronkov, A., Kov\u00e1cs, L., Bhayat, A., Gleiss, B., Hajdu, M., Hozzova, P., Evgeny\u00a0Kotelnikov, J.R., Rawson, M., Riener, M., Robillard, S., Schoisswohl, J.: Vampire 4.7-SMT System Description. https:\/\/smt-comp.github.io\/2022\/system-descriptions\/Vampire.pdf (2022)"},{"key":"33_CR36","doi-asserted-by":"publisher","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving Quantified Linear Arithmetic by Counterexample-Guided Instantiation. FMSD 51(3), 500\u2013532 (2017), https:\/\/doi.org\/10.1007\/s10703-017-0290-y","DOI":"10.1007\/s10703-017-0290-y"},{"key":"33_CR37","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovic, P.: Faster, Higher, Stronger: E 2.3. In: CADE, LNCS, vol. 11716, pp. 495\u2013507, Springer (2019), https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"33_CR38","doi-asserted-by":"publisher","unstructured":"Voronkov, A.: AVATAR: The Architecture for First-Order Theorem Provers. In: CAV, LNCS, vol. 8559, pp. 696\u2013710, Springer (2014), https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"33_CR39","doi-asserted-by":"publisher","unstructured":"Waldmann, U.: Extending Reduction Orderings to ACU-Compatible Reduction Orderings. Inf. Process. Lett. 67(1), 43\u201349 (1998), https:\/\/doi.org\/10.1016\/S0020-0190(98)00084-2","DOI":"10.1016\/S0020-0190(98)00084-2"},{"key":"33_CR40","doi-asserted-by":"publisher","unstructured":"Waldmann, U.: Superposition for Divisible Torsion-Free Abelian Groups. In: CADE, LNCS, vol. 1421, pp. 144\u2013159, Springer (1998), https:\/\/doi.org\/10.1007\/BFb0054257","DOI":"10.1007\/BFb0054257"},{"key":"33_CR41","doi-asserted-by":"publisher","unstructured":"Yamada, A., Winkler, S., Hirokawa, N., Middeldorp, A.: AC-KBO Revisited. Theory Pract. Log. Program. 16(2), 163\u2013188 (2016), https:\/\/doi.org\/10.1017\/S1471068415000083","DOI":"10.1017\/S1471068415000083"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:05:28Z","timestamp":1781024728000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}