Querying Guarded Fragments via Resolution
The problem of answering Boolean conjunctive queries over the guarded fragment is decidable, however, as yet no practical decision procedure exists. In this paper, we present a resolution-based decision procedure to address this problem, and further extend the decision procedure to the loosely guarded fragment. In particular, we show that using a separation rule and top-variable-based techniques, one can rewrite Boolean conjunctive queries into a set of (loosely) guarded clauses, so that querying the (loosely) guarded fragment can be reduced to deciding the (loosely) guarded fragment. As far as we know, this is the first practical decision procedure for answering Boolean conjunctive queries over the guarded fragment and the loosely guarded fragment.
READ FULL TEXT