Guarded negation

We consider restrictions of first-order logic and least fixpoint logic in which all
occurrences of negation are required to be guarded by an atomic predicate.
The so obtained guarded negation fragments GNFO and GNFP naturally extend
the well-known guarded fragments GFO and GFP, as well as the unary negation
fragments UNFO and UNFP of FO and LFP, respectively.
The latter were recently introduced by ten Cate and Segoufin [STACS'11] based
on the novel idea of constraining the use of negation instead of quantification
(which has had more currency in the theory of databases).
  The expressive power of the guarded negation fragments can be characterized
in terms of invariance under an appropriate notion of bisimulation. It follows that
GNFO and GNFP possess the tree-like model property. We show that the
satisfiability problems of GNFO and GNFP are 2ExpTime-complete and that
GNFO has the finite (smallish) model property.
  These results are obtained via reduction to the respective guarded fragments
based on a refinement of the approach of [B.,Gottlob,Otto LICS'10] for the solution
of query answering against guarded theories in the finite. The same translation
reduces the finite satisfiability problem for GNFP to that of guarded fixpoint logic,
a problem recently shown decidable by Bojanczyk and myself.
  I will briefly discuss the model checking complexity of GNFO and GNFP and
mention the Craig interpolation property of GNFO, which are arrived at by lifting
them from the unary negation fragments.