2013/09/23 by Luc Segoufin, Balder ten Cate
Computer Science · Mathematics · #Algorithm #Boolean satisfiability problem #Computer science #Decidability #Description logic #Discrete mathematics #Formal Methods in Verification #Fragment (logic) #Higher-order logic #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Modal #Modal logic #Monadic predicate calculus #Negation #Programming language #Rotation formalisms in three dimensions #Satisfiability #Unary operation #cs.LO
paper · pdf · doi:10.2168/lmcs-9(3:25)2013
published as Logical Methods in Computer Science, Volume 9, Issue 3 (September 24, 2013) lmcs:792 · 2 figures
arxiv created 2013/09/23 · openalex publication_date 2013/09/24 · arxiv updated 2015/07/01 · openalex created_date 2020/07/02 · openalex updated_date 2026/08/05
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.