Guarded Negation
Vince Barany (Darmstadt)
Info
|
Date |
18th August 2011 |
|
Time |
11:30 |
|
Place |
380 |
Abstract
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].
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 combined
complexity bounds for model
checking the guarded negation fragments, and conclude with some outstanding
questions.
This is joint work with Balder ten Cate and Luc Segoufin [ICALP'11], and
with Mikolaj Bojanczyk [arXiv'11
/ IPL].
Further info
|
Related series |
|
