Download PDFOpen PDF in browserCurrent version

ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version)

EasyChair Preprint 9606, version 3

Versions: 12345history
45 pagesDate: January 27, 2023

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.

This paper is an extended version of the paper ``ALASCA: Reasoning in Quantified Linear Arithmetic'' published at TACAS 2023, written by the same set of the authors. In this extended version we provide the formal proofs of the results from our TACAS 2023 paper

Keyphrases: Quantified First-Order Logic, SMT, automated reasoning, linear arithmetic, theorem proving

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:9606,
  author    = {Konstantin Korovin and Laura Kovacs and Giles Reger and Johannes Schoisswohl and Andrei Voronkov},
  title     = {ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version)},
  howpublished = {EasyChair Preprint 9606},
  year      = {EasyChair, 2023}}
Download PDFOpen PDF in browserCurrent version