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

Record link:

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

Title:

ALASCA: Reasoning in Quantified Linear Arithmetic

Citation:

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

Publisher DOI:

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

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

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

Organisational Unit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering

Published in:

Tools and Algorithms for the Construction and Analysis of Systems

ISBN:

978-3-031-30823-9

Volume:

13993

DOI of the book:

10.1007/978-3-031-30823-9

Date (published):

2023

Event name:

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

Event date:

24-Apr-2023 - 27-Apr-2023

Event place:

Paris, France

Number of Pages:

Publisher:

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.

Project title:

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)

Project (external):

EPSRC

Project ID:

EP/V000497/1

Research Areas:

Logic and Computation: 100%

Science Branch:

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

License:

CC BY 4.0