Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments

TL;DR

This paper introduces new saturation-based procedures for Boolean conjunctive query answering and rewriting in guarded fragments, improving decision procedures and enabling efficient querying over distributed datasets.

Contribution

It develops the first automated deduction decision procedures and saturation-based rewriting methods for guarded, loosely guarded, and clique-guarded fragments.

Findings

Improved resolution-based decision procedures for guarded fragments

First saturation-based query rewriting for these fragments

Procedures handle distributed dataset querying efficiently

Abstract

Query answering is an important problem in AI, database and knowledge representation. In this paper, we develop saturation-based Boolean conjunctive query answering and rewriting procedures for the guarded, the loosely guarded and the clique-guarded fragments. Our query answering procedure improves existing resolution-based decision procedures for the guarded and the loosely guarded fragments and this procedure solves Boolean conjunctive query answering problems for the guarded, the loosely guarded and the clique-guarded fragments. Based on this query answering procedure, we also introduce a novel saturation-based query rewriting procedure for these guarded fragments. Unlike mainstream query answering and rewriting methods, our procedures derive a compact and reusable saturation, namely a closure of formulas, to handle the challenge of querying for distributed datasets. This paper lays the theoretical foundations for the first automated deduction decision procedures for Boolean conjunctive query answering and the first saturation-based Boolean conjunctive query rewriting in the guarded, the loosely guarded and the clique-guarded fragments.