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.
翻译:查询回答是人工智能、数据库和知识表示领域中的一个重要问题。本文针对守护片段、松散守护片段和团守护片段,开发了基于饱和的布尔合取查询回答与重写程序。我们的查询回答程序改进了现有基于归结的守护片段和松散守护片段判定程序,并解决了守护片段、松散守护片段和团守护片段中的布尔合取查询回答问题。基于此查询回答程序,我们还为这些守护片段引入了一种新颖的基于饱和的查询重写程序。与主流的查询回答与重写方法不同,我们的程序推导出紧凑且可重复使用的饱和结构(即公式闭包),以应对分布式数据集查询的挑战。本文为守护片段、松散守护片段和团守护片段中的首个布尔合取查询回答自动演绎判定程序以及首个基于饱和的布尔合取查询重写奠定了理论基础。