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

Sen Zheng (Corresponding), Renate A. Schmidt

Research output: Contribution to journalArticlepeer-review

20 Downloads (Pure)

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.
Original languageEnglish
Article number39
Number of pages68
JournalJournal of Automated Reasoning
Volume67
DOIs
Publication statusPublished - 23 Nov 2023

Keywords

  • Saturation-based decision procedure
  • query answering
  • saturation-based query rewriting
  • the guarded quantification fragments

Fingerprint

Dive into the research topics of 'Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments'. Together they form a unique fingerprint.

Cite this