Skip to Main content Skip to Navigation
Conference papers

On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic

Matthias Horbach 1 Marco Voigt 1, 2, 3 Christoph Weidenbach 1, 3
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
Abstract : In general, first-order predicate logic extended with linear integer arithmetic is undecidable. We show that the Bernays-Schönfinkel-Ramsey fragment (∃ * ∀ *-sentences) extended with a restricted form of linear integer arithmetic is decidable via finite ground instantiation. The identified ground instances can be employed to restrict the search space of existing automated reasoning procedures considerably, e.g., when reasoning about quantified properties of array data structures formalized in Bradley, Manna, and Sipma's array property fragment. Typically, decision procedures for the array property fragment are based on an exhaustive instantiation of universally quantified array indices with all the ground index terms that occur in the formula at hand. Our results reveal that one can get along with significantly fewer instances.
Document type :
Conference papers
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download
Contributor : Stephan Merz <>
Submitted on : Wednesday, September 27, 2017 - 6:54:51 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Long-term archiving on: : Thursday, December 28, 2017 - 12:20:02 PM


Files produced by the author(s)




Matthias Horbach, Marco Voigt, Christoph Weidenbach. On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic. CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. pp.77-94, ⟨10.1007/978-3-319-63046-5_6⟩. ⟨hal-01592160⟩



Record views


Files downloads