ALASCA: Reasoning in Quantified Linear Arithmetic

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

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


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 languageEnglish
Title of host publicationProceedings of the 29th on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23)
PublisherSpringer Cham
ISBN (Electronic)978-3-031-30823-9
ISBN (Print)978-3-031-30822-2
Publication statusPublished - 22 Apr 2023

Publication series

NameTools and Algorithms for the Construction and Analysis of Systems
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


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


Dive into the research topics of 'ALASCA: Reasoning in Quantified Linear Arithmetic'. Together they form a unique fingerprint.

Cite this