Unary negation

Balder Ten Cate 1 Luc Segoufin 2
2 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 study fragments of first-order logic and of least fixed point logic that allow only unary negation: negation of formulas with at most one free variable. These logics generalize many interesting known formalisms, including modal logic and the µ-calculus, as well as conjunctive queries and monadic Datalog. We show that satisfiability and finite satisfiability are decidable for both fragments, and we pinpoint the complexity of satisfiability, finite satisfiability, and model checking. We also show that the unary negation fragment of first-order logic is model-theoretically very well behaved. In particular, it enjoys Craig Interpolation and the Projective Beth Property.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (3)
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00904567
Contributeur : Luc Segoufin <>
Soumis le : jeudi 14 novembre 2013 - 16:54:46
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : samedi 15 février 2014 - 04:36:42

Fichier

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

Identifiants

  • HAL Id : hal-00904567, version 1

Collections

Citation

Balder Ten Cate, Luc Segoufin. Unary negation. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (3). 〈hal-00904567〉

Partager

Métriques

Consultations de la notice

249

Téléchargements de fichiers

114