Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete

Abstract : Linear arithmetic extended with free predicate symbols is undecidable, in general. We show that the restriction of linear arithmetic inequations to simple bounds extended with the Bernays-Schönfinkel-Ramsey free first-order fragment is decidable and NEXPTIME-complete. The result is almost tight because the Bernays-Schönfinkel-Ramsey fragment is undecidable in combination with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations.
Type de document :
Autre publication
preprint. 2015
Liste complète des métadonnées

https://hal.inria.fr/hal-01239399
Contributeur : Stephan Merz <>
Soumis le : lundi 7 décembre 2015 - 17:27:21
Dernière modification le : lundi 20 novembre 2017 - 15:14:02

Identifiants

  • HAL Id : hal-01239399, version 1
  • ARXIV : 1501.07209

Collections

Citation

Marco Voigt, Christoph Weidenbach. Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete. preprint. 2015. 〈hal-01239399〉

Partager

Métriques

Consultations de la notice

91