ALASCA: Reasoning in Quantified Linear Arithmetic

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

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

ALASCA: Reasoning in Quantified Linear Arithmetic

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

Formal Methods

Research output: Chapter in Book/Conference proceeding › Chapter › peer-review

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 calculus that lifts superposition reasoning to the linear arithmetic domain. We show that is both sound and complete with respect to an axiomatisation of linear arithmetic. We implemented and evaluated using the VAMPIRE theorem prover, solving many more challenging problems compared to state-of-the-art reasoners.

Original language	English
Title of host publication	Proceedings of the 29th on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23)
Publisher	Springer Cham
Pages	647-665
ISBN (Electronic)	978-3-031-30823-9
ISBN (Print)	978-3-031-30822-2
DOIs	https://doi.org/10.1007/978-3-031-30823-9_33
Publication status	Published - 22 Apr 2023

Publication series

Name	Tools and Algorithms for the Construction and Analysis of Systems
Volume	13993
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords

Automated Reasoning
Linear Arithmetic
SMT
quantifed First-Order Logic
Theorem Proving

Access to Document

10.1007/978-3-031-30823-9_33Licence: CC BY

SCorCH: Secure Code for Capability Hardware
Reger, G. (PI), Cordeiro, L. (CoI), Korovin, K. (CoI), Mustafa, M. (CoI) & Olivier, P. (CoI)
1/07/20 → 31/12/23
Project: Research

Cite this

Korovin, K., Kovács, L., Reger, G., Schoisswohl, J., & Voronkov, A. (2023). ALASCA: Reasoning in Quantified Linear Arithmetic. In Proceedings of the 29th on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23) (pp. 647-665). Article Chapter 33 (Tools and Algorithms for the Construction and Analysis of Systems; Vol. 13993). Springer Cham. https://doi.org/10.1007/978-3-031-30823-9_33

@inbook{17270168928e4dadbcb159bb73d44317,

title = "ALASCA: Reasoning in Quantified Linear Arithmetic",

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 calculus that lifts superposition reasoning to the linear arithmetic domain. We show that is both sound and complete with respect to an axiomatisation of linear arithmetic. We implemented and evaluated using the VAMPIRE theorem prover, solving many more challenging problems compared to state-of-the-art reasoners.",

keywords = "Automated Reasoning, Linear Arithmetic, SMT, quantifed First-Order Logic, Theorem Proving",

author = "Konstantin Korovin and Laura Kov{\'a}cs and Giles Reger and Johannes Schoisswohl and Andrei Voronkov",

year = "2023",

month = apr,

day = "22",

doi = "10.1007/978-3-031-30823-9_33",

language = "English",

isbn = "978-3-031-30822-2",

series = "Tools and Algorithms for the Construction and Analysis of Systems",

publisher = "Springer Cham",

pages = "647--665",

booktitle = "Proceedings of the 29th on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23)",

address = "Switzerland",

}

Korovin, K, Kovács, L, Reger, G, Schoisswohl, J & Voronkov, A 2023, ALASCA: Reasoning in Quantified Linear Arithmetic. in Proceedings of the 29th on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23)., Chapter 33, Tools and Algorithms for the Construction and Analysis of Systems, vol. 13993, Springer Cham, pp. 647-665. https://doi.org/10.1007/978-3-031-30823-9_33

ALASCA: Reasoning in Quantified Linear Arithmetic. / Korovin, Konstantin; Kovács, Laura; Reger, Giles et al.
Proceedings of the 29th on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23). Springer Cham, 2023. p. 647-665 Chapter 33 (Tools and Algorithms for the Construction and Analysis of Systems; Vol. 13993).

Research output: Chapter in Book/Conference proceeding › Chapter › peer-review

TY - CHAP

T1 - ALASCA: Reasoning in Quantified Linear Arithmetic

AU - Korovin, Konstantin

AU - Kovács, Laura

AU - Reger, Giles

AU - Schoisswohl, Johannes

AU - Voronkov, Andrei

PY - 2023/4/22

Y1 - 2023/4/22

N2 - 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 calculus that lifts superposition reasoning to the linear arithmetic domain. We show that is both sound and complete with respect to an axiomatisation of linear arithmetic. We implemented and evaluated using the VAMPIRE theorem prover, solving many more challenging problems compared to state-of-the-art reasoners.

AB - 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 calculus that lifts superposition reasoning to the linear arithmetic domain. We show that is both sound and complete with respect to an axiomatisation of linear arithmetic. We implemented and evaluated using the VAMPIRE theorem prover, solving many more challenging problems compared to state-of-the-art reasoners.

KW - Automated Reasoning

KW - Linear Arithmetic

KW - SMT

KW - quantifed First-Order Logic

KW - Theorem Proving

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

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

M3 - Chapter

SN - 978-3-031-30822-2

T3 - Tools and Algorithms for the Construction and Analysis of Systems

SP - 647

EP - 665

BT - Proceedings of the 29th on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23)

PB - Springer Cham

ER -

ALASCA: Reasoning in Quantified Linear Arithmetic

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Projects

SCorCH: Secure Code for Capability Hardware

Cite this