When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2011.344
URN: urn:nbn:de:0030-drops-30256
Go to the corresponding LIPIcs Volume Portal

ten Cate, Balder ; Segoufin, Luc

Unary negation

Document 1.pdf (686 KB)


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 mu-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 Beth property.

BibTeX - Entry

  author =	{Balder ten Cate and Luc Segoufin},
  title =	{{Unary negation}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011) },
  pages =	{344--355},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Thomas Schwentick and Christoph D{\"u}rr},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-30256},
  doi =		{},
  annote =	{Keywords: Decidability, Logic, Unary negation}

Keywords: Decidability, Logic, Unary negation
Seminar: 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)
Issue Date: 2011
Date of publication: 11.03.2011

DROPS-Home | Fulltext Search | Imprint Published by LZI