10.4230/LIPICS.STACS.2011.344
ten Cate, Balder
Balder
ten Cate
Segoufin, Luc
Luc
Segoufin
Unary negation
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
Decidability
Logic
Unary negation
Schwentick, Thomas
Thomas
Schwentick
Dürr, Christoph
Christoph
Dürr
2011
2011-03-11
2011-03-11
2011-03-11
en
urn:nbn:de:0030-drops-30256
10.4230/LIPIcs.STACS.2011
978-3-939897-25-5
1868-8969
10.4230/LIPIcs.STACS.2011
LIPIcs, Volume 9, STACS 2011
28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)
2013
9
29
344
355
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Schwentick, Thomas
Thomas
Schwentick
Dürr, Christoph
Christoph
Dürr
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
9
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
12 pages
702785 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
LIPIcs, Vol. 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011), pages 344-355