
We consider restrictions of first-order logic and of fixpoint logic in which all occurrences of negation are required to be guarded by an atomic predicate. In terms of expressive power, the logics in question, called GNFO and GNFP, extend the guarded fragment of first-order logic and the guarded least fixpoint logic, respectively. They also extend the recently introduced unary negation fragments of first-order logic and of least fixpoint logic. We show that the satisfiability problem for GNFO and for GNFP is 2ExpTime-complete, both on arbitrary structures and on finite structures. We also study the complexity of the associated model checking problems. Finally, we show that GNFO and GNFP are not only computationally well behaved, but also model theoretically: we show that GNFO and GNFP have the tree-like model property and that GNFO has the finite model property, and we characterize the expressive power of GNFO in terms of invariance for an appropriate notion of bisimulation. Our complexity upper bounds for GNFO and GNFP hold true even for their “clique-guarded” extensions CGNFO and CGNFP, in which clique guards are allowed in the place of guards.
Logic in computer science, Specification and verification (program logics, model checking, etc.), fixpoint logic, Analysis of algorithms and problem complexity, guarded fragment, Fixpoint Logic, decidability, Decidability, [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], satisfiability, negation, Guarded Fragment, Satisfiability, Negation, Modal logic (including the logic of norms), first-order logic
Logic in computer science, Specification and verification (program logics, model checking, etc.), fixpoint logic, Analysis of algorithms and problem complexity, guarded fragment, Fixpoint Logic, decidability, Decidability, [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], satisfiability, negation, Guarded Fragment, Satisfiability, Negation, Modal logic (including the logic of norms), first-order logic
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 53 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
