An important class of decidable first-order logic fragments are those satisfying a guardedness condition, such as the guarded fragment (GF). Usually, decidability for these logics is closely linked to the tree-like model property - the fact that satisfying models can be taken to have tree-like form. Decision procedures for the guarded fragment based on the tree-like model property are difficult to implement. An alternative approach, based on restricting first-order resolution, has been proposed, and this shows more promise from the point of view of implementation. In this work, we connect the tree-like model property of the guarded fragment with the resolution-based approach. We derive efficient resolution-based rewriting algorithms that solve the Quantifier-Free Query Answering Problem under Guarded Tuple Generating Dependencies (GTGDs) and Disjunctive Guarded Tuple Generating Dependencies (DisGTGDs). The Query Answering Problem for these classes subsumes many cases of GF satisfiability. Our algorithms, in addition to making the connection to the tree-like model property clear, give a natural account of the selection and ordering strategies used by resolution procedures for the guarded fragment. We also believe that our rewriting algorithm for the special case of GTGDs may prove itself valuable in practice as it does not require any Skolemisation step and its theoretical runtime outperforms those of known GF resolution procedures in case of fixed dependencies. Moreover, we show a novel normalisation procedure for the widely used chase procedure in case of (disjunctive) GTGDs, which could be useful for future studies.
翻译:一种重要的分解第一阶逻辑碎片类别是那些满足了保密性条件(例如,有防守的碎片 ) 的重要类别。通常,这些逻辑的分解性与树类模型属性密切相连,即满足模型可以采取树类相似的形式。基于树类模型属性的保密碎片决定程序难以实施。基于限制一阶分辨率的替代方法已经提出,从执行角度看,这显示了更多的希望。在这项工作中,我们将保守碎片的像树类模型属性与基于解决方案的方法联系起来。我们获取基于解决方案的高效正常写法,在有防守的图类衍生依赖(GGGGGDs)和有防守的图类依赖(DGTGGDs)下,可以解决。对于这些类别来说,解答问题的问题的解答能力是很多次的。除了与像树类的模型属性的分级方法连接之外,我们还获得了基于解决方案的基于解决方案的正常写法演算算法,我们用了一个宝贵的解算法程序来证明,我们用这些分解的分解法的分解程序,我们用了任何分解的分解程序。