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

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

Publication series

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

Keywords

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

Fingerprint

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

Cite this