The Bernays–Schönfinkel–Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable

Abstract : First-order linear real arithmetic enriched with uninterpreted predicate symbols yields an interesting modeling language. However, satisfiability of such formulas is undecidable, even if we restrict the uninterpreted predicate symbols to arity one. In order to find decidable fragments of this language, it is necessary to restrict the expressiveness of the arithmetic part. One possible path is to confine arithmetic expressions to difference constraints of the form x − y R c, where R ranges over the standard relations <, ≤, =, =, ≥, > and x, y are universally quantified. However, it is known that combining difference constraints with uninterpreted predicate symbols yields an undecidable satisfiability problem again. In this paper, it is shown that satisfiability becomes decidable if we in addition bound the ranges of universally quantified variables. As bounded intervals over the reals still comprise infinitely many values, a trivial instantiation procedure is not sufficient to solve the problem.
Type de document :
Communication dans un congrès
Clare Dixon and Marcelo Finger. FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. Springer, 10483, pp.244-261, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66167-4_14〉
Liste complète des métadonnées

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

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

Fichier

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

Identifiants

Collections

Citation

Marco Voigt. The Bernays–Schönfinkel–Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable. Clare Dixon and Marcelo Finger. FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. Springer, 10483, pp.244-261, 2017, Lecture Notes in Computer Science. 〈10.1007/978-3-319-66167-4_14〉. 〈hal-01592169〉

Partager

Métriques

Consultations de la notice

57

Téléchargements de fichiers

8