The semijoin algebra and the guarded fragment

Deciding the Loosely Guarded Fragment and Querying Its Horn Fragment Using Resolution

We consider the following query answering problem: Given a Boolean conjunctive query and a theory in the Horn loosely guarded fragment, the aim is to determine whether the query is entailed by the theory. In this paper, we present a resolution decision procedure for the loosely guarded fragment, and use such a procedure to answer Boolean conjunctive queries against the Horn loosely guarded fragment. The Horn loosely guarded fragment subsumes classes of rules that are prevalent in ontology-based query answering, such as Horn ALCHOI and guarded existential rules. Additionally, we identify star q…

基于饱和的布尔合取查询回答与重写：面向有保护量化片段

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

本文提出基于饱和的布尔合取查询回答与重写程序，适用于有保护、松散有保护和团有保护片段，改进现有消解方法，并首次实现分布式数据集上的紧凑可复用饱和闭包。研究为自动化演绎决策和查询重写奠定理论基础。

Querying the Guarded Fragment

Evaluating a Boolean conjunctive query Q against a guarded first-order theory F is equivalent to checking whether "F and not Q" is unsatisfiable. This problem is relevant to the areas of database theory and description logic. Since Q may not be guarded, well known results about the decidability, complexity, and finite-model property of the guarded fragment do not obviously carry over to conjunctive query answering over guarded theories, and had been left open in general. By investigating finite guarded bisimilar covers of hypergraphs and relational structures, and by substantially generalising…

Decision Procedures for Guarded Logics

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 …

Dichotomies in Ontology-Mediated Querying with the Guarded Fragment

We study the complexity of ontology-mediated querying when ontologies are formulated in the guarded fragment of first-order logic (GF). Our general aim is to classify the data complexity on the level of ontologies where query evaluation w.r.t. an ontology O is considered to be in PTime if all (unions of conjunctive) queries can be evaluated in PTime w.r.t. O and coNP-hard if at least one query is coNP-hard w.r.t. O. We identify several large and relevant fragments of GF that enjoy a dichotomy between PTime and coNP, some of them additionally admitting a form of counting. In fact, almost all on…

guarded negation transitive closure logic

Guarded Negation Transitive Closure Logic

本文研究了guarded negation fragment of transitive closure logic (GNTC) 的可满足性问题，证明其为2ExpTime-完全，并展示了该逻辑的模型检查问题在组合复杂度下为P^NP[O(log^2 n)]-完全。