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

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.
Type de document :
Communication dans un congrès
Leonardo de Moura. CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, 10395, pp.77-94, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-63046-5_6〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01592160
Contributeur : Stephan Merz <>
Soumis le : mercredi 27 septembre 2017 - 18:54:51
Dernière modification le : lundi 20 novembre 2017 - 15:14:02

Fichier

HorbachVoigtWeidenbachCADE.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Matthias Horbach, Marco Voigt, Christoph Weidenbach. On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic. Leonardo de Moura. CADE 26 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. Springer, 10395, pp.77-94, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-63046-5_6〉. 〈hal-01592160〉

Partager

Métriques

Consultations de la notice

90

Téléchargements de fichiers

11