Document Open Access Logo

Unary negation

Authors Balder ten Cate, Luc Segoufin

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2011.344.pdf
  • Filesize: 0.67 MB
  • 12 pages

Document Identifiers

Subject Classification

Keywords
  • Decidability
  • Logic
  • Unary negation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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 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.

Cite As Get BibTex

Balder ten Cate and Luc Segoufin. Unary negation. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 344-355, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011) https://doi.org/10.4230/LIPIcs.STACS.2011.344

Author Details

Balder ten Cate
Luc Segoufin
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact
OSZAR »