2026-08-13T19:54:39Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3025 2024-03-06T10:33:45Z ddc:004 open_access

Unary negation ten Cate, Balder Segoufin, Luc Decidability Logic Unary negation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Balder ten Cate and Luc Segoufin 2011 Is Part Of LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2011.344 urn:nbn:de:0030-drops-30256 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.344 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode