ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version)

EasyChair Preprint 9606, version 2

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

@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}}