Luc Segoufin ; Balder ten Cate - Unary negation

lmcs:792 - Logical Methods in Computer Science, September 24, 2013, Volume 9, Issue 3 - https://doi.org/10.2168/LMCS-9(3:25)2013
Unary negationArticle

Authors: Luc Segoufin ; Balder ten Cate

    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 Projective Beth Property.


    Volume: Volume 9, Issue 3
    Published on: September 24, 2013
    Imported on: January 16, 2013
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • III: Medium: Data Interoperability via Schema Mappings; Funder: National Science Foundation; Code: 0905276
    • Foundations of Web Data Management; Funder: European Commission; Code: 226513
    • III: Small: Aspects of Integrating Heterogeneous and Inconsistent Data; Funder: National Science Foundation; Code: 1217869

    8 Documents citing this article

    Consultation statistics

    This page has been seen 1644 times.
    This article's PDF has been downloaded 422 times.