Querying the Guarded Fragment

Evaluating a boolean conjunctive query q over a guarded first-order
theory T is equivalent to checking whether (T & not q) is unsatisfiable.
This problem is relevant to the areas of database theory and
description logic. Since q may not be guarded, well known results
about the decidability, complexity, and finite-model property of the
guarded fragment do not obviously carry over to conjunctive query
answering over guarded theories, and had been left open in general.
Extending Rosati's finite chase we construct finite guarded bisimilar
covers of hypergraphs and relational structures such that the projection
of any small substructure of the cover is tree decomposable in the
base structure. Thus we prove for guarded theories T and UCQs q that
(i) T implies q iff T implies q over finite models; and observe that
(ii) answering UCQs over guarded theories is {2EXPTIME}-complete.
The construction is merely polynomial under reasonable restrictions,
also yielding (iii) existence of polynomial-size conformal covers of
hypergraphs of bounded width; (iv) a new proof of the finite model
property of the clique-guarded fragment; (v) the small model property
of the (clique) guarded fragment with optimal bounds; (vi) a PTIME
solution to the canonisation problem modulo guarded bisimulation,
which yields (vii) a capturing result for guarded-bisimulation-invariant
fragment of PTIME.

This is joint work with Georg Gottlob and Martin Otto.