Unary negation
Logical Methods in Computer Science(2013)
摘要
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.
更多查看译文
关键词
computer science - logic in computer science
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络