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

Answering Boolean conjunctive query over logical constraints is an essential problem in knowledge representation. Other problems in computer science such as constraint satisfaction and homomorphism problems can also be seen as Boolean conjunctive query answering problems. This paper develops saturation-based Boolean conjunctive query answering and rewriting procedures for the guarded, the loosely guarded and the clique guarded fragments. We improve existing resolution-based decision procedures for the guarded and the loosely guarded fragments, and devise a saturation-based approach deciding Boolean conjunctive query answering problems for the guarded, the loosely guarded and the clique guarded fragments. Based on the saturation-based query answering procedure, we introduce a novel saturation-based query rewriting setting that aims to back-translate the saturated clausal set derived from saturation-based query answering procedures, to a (Skolem-symbol-free) first-order formula, and devise a saturation-based query rewriting procedures for all these guarded fragments. Unlike mainstream query answering and rewriting approaches, our procedures derive a compact saturation that is reusable even if the data changes. This paper lays the theoretical foundations for the first practical Boolean conjunctive query answering and the first saturation-based Boolean conjunctive query rewriting procedures for the guarded, the loosely guarded and the clique guarded fragments.