Guarded negation

Vince Barany 1 Balder Ten Cate 2 Luc Segoufin 1
1 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We consider restrictions of first-order logic and of fixpoint logic in which all occurrences of negation are required to be guarded by an atomic predicate. In terms of expressive power, the logics in question, called GNFO and GNFP, extend the guarded fragment of first-order logic and the guarded least fixpoint logic, respectively. They also extend the recently introduced unary negation fragments of first-order logic and of least fixpoint logic. We show that the satisfiability problem for GNFO and for GNFP is 2ExpTime-complete, both on arbitrary structures and on finite structures. We also study the complexity of the associated model checking problems. Finally, we show that GNFO and GNFP are not only computationally well behaved, but also model theoretically: we show that GNFO and GNFP have the tree-like model property and that GNFO has the finite model property, and we characterize the expressive power of GNFO in terms of invariance for an appropriate notion of bisimulation. Our complexity upper bounds for GNFO and GNFP hold true even for their " clique-guarded " extensions CGNFO and CGNFP, in which clique guards are allowed in the place of guards.
Type de document :
Article dans une revue
Journal of the ACM (JACM), Association for Computing Machinery, 2015, 62 (3), pp.24
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01184763
Contributeur : Luc Segoufin <>
Soumis le : mercredi 26 août 2015 - 12:12:27
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : vendredi 27 novembre 2015 - 10:54:59

Fichier

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

Identifiants

  • HAL Id : hal-01184763, version 1

Citation

Vince Barany, Balder Ten Cate, Luc Segoufin. Guarded negation. Journal of the ACM (JACM), Association for Computing Machinery, 2015, 62 (3), pp.24. 〈hal-01184763〉

Partager

Métriques

Consultations de la notice

175

Téléchargements de fichiers

81