Projects per year
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. Firstorder 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 stateoftheart 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  647665 
ISBN (Electronic)  9783031308239 
ISBN (Print)  9783031308222 
DOIs  
Publication status  Published  22 Apr 2023 
Publication series
Name  Tools and Algorithms for the Construction and Analysis of Systems 

Volume  13993 
ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Keywords
 Automated Reasoning
 Linear Arithmetic
 SMT
 quantifed FirstOrder Logic
 Theorem Proving
Fingerprint
Dive into the research topics of 'ALASCA: Reasoning in Quantified Linear Arithmetic'. Together they form a unique fingerprint.Projects
 1 Finished

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