Unary negation - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Logical Methods in Computer Science Année : 2013

Unary negation

Résumé

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.
Fichier principal
Vignette du fichier
unaryneg.pdf (509.53 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00904567 , version 1 (14-11-2013)

Identifiants

  • HAL Id : hal-00904567 , version 1

Citer

Balder Ten Cate, Luc Segoufin. Unary negation. Logical Methods in Computer Science, 2013, 9 (3). ⟨hal-00904567⟩
159 Consultations
88 Téléchargements

Partager

Gmail Facebook X LinkedIn More