<div class="csl-bib-body">
<div class="csl-entry">Korovin, K., Kovács, L., Reger, G., Schoisswohl, J., & Voronkov, A. (2023). ALASCA: Reasoning in Quantified Linear Arithmetic. In S. Sankaranarayanan & N. Sharygina (Eds.), <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (pp. 647–665). Springer. https://doi.org/10.1007/978-3-031-30823-9_33</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/193074
-
dc.description.abstract
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 ALASCA calculus that lifts superposition reasoning to the linear arithmetic domain. We show that ALASCA is both sound and complete with respect to an axiomatisation of linear arithmetic. We implemented and evaluated ALASCA using the Vampire theorem prover, solving many more challenging problems compared to state-of-the-art reasoners.
en
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
Automated Reasoning
en
dc.subject
Linear Arithmetic
en
dc.subject
Quantified First-Order Logic
en
dc.subject
SMT
en
dc.subject
Theorem Proving
en
dc.title
ALASCA: Reasoning in Quantified Linear Arithmetic
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.editoraffiliation
University of Colorado Boulder, United States of America (the)
