ALASCA: Reasoning in Quantified Linear Arithmetic

Korovin, Konstantin; Kovács, Laura; Reger, Giles; Schoisswohl, Johannes; Voronkov, Andrei

doi:10.1007/978-3-031-30823-9_33

Datensatz Zitierlink:

http://hdl.handle.net/20.500.12708/193074

Titel:

ALASCA: Reasoning in Quantified Linear Arithmetic

Zitat:

Korovin, K., Kovács, L., Reger, G., Schoisswohl, J., & Voronkov, A. (2023). ALASCA: Reasoning in Quantified Linear Arithmetic. In S. Sankaranarayanan & N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 647–665). Springer. https://doi.org/10.1007/978-3-031-30823-9_33

CatalogPlus:

AC17204987

Verlags-DOI:

10.1007/978-3-031-30823-9_33

Publikationstyp:

Konferenzbeitrag - Full-Paper Contribution

Sprache:

Englisch

Autor_innen:

Korovin, Konstantin
Kovács, Laura
Reger, Giles
Schoisswohl, Johannes
Voronkov, Andrei

Organisationseinheit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering

Erschienen in:

Tools and Algorithms for the Construction and Analysis of Systems

ISBN:

978-3-031-30823-9

Band:

13993

DOI des Buches:

10.1007/978-3-031-30823-9

Datum (veröffentlicht):

2023

Veranstaltungsname:

TACAS – 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Veranstaltungszeitraum:

24-Apr-2023 - 27-Apr-2023

Veranstaltungsort:

Paris, Frankreich

Umfang:

Verlag:

Springer

Keywords:

Automated Reasoning; Linear Arithmetic; Quantified First-Order Logic; SMT; Theorem Proving

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.

Projekttitel:

Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission)
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 85 (FWF - Österr. Wissenschaftsfonds)

Projekt (extern):

EPSRC

Projektnummer:

EP/V000497/1

Forschungsschwerpunkte:

Logic and Computation: 100%

Wissenschaftszweig:

1020 - Informatik: 80%
1010 - Mathematik: 20%

Lizenz:

CC BY 4.0