English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Paper

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

MPS-Authors
/persons/resource/persons44642

Horbach,  Matthias
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons101767

Voigt,  Marco
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45719

Weidenbach,  Christoph       
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

arXiv:1705.08792.pdf
(Preprint), 403KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Horbach, M., Voigt, M., & Weidenbach, C. (2017). On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic. Retrieved from http://arxiv.org/abs/1705.08792.


Cite as: https://hdl.handle.net/11858/00-001M-0000-002D-8140-2
Abstract
In general, first-order predicate logic extended with linear integer arithmetic is undecidable. We show that the Bernays-Sch\"onfinkel-Ramsey fragment ($\exists^* \forall^*$-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.