arXiv subjects

Sen Zheng

Publications and source records attributed to Sen Zheng.

3 recordsLinked to original sources

arXiv2022

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

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.

cs.DB↗

arXiv2020

Querying Guarded Fragments via Resolution

Answering Boolean conjunctive queries over the guarded fragment is decidable, however, as yet no practical decision procedure exists. Meanwhile, ordered resolution, as a practically oriented algorithm, is widely used in state-of-art modern theorem provers. In this paper, we devise a resolution decision procedure, which not only proves decidability of querying of the guarded fragment, but is implementable in any `off-the-shelf' resolution theorem prover with modest effort. Further, we extend the procedure to querying the loosely guarded fragment. The difficulty in querying a knowledge base of (loosely) guarded clauses is that query clauses are not guarded. We show however there are ways to reformulate query clauses into (loosely) guarded clauses either directly via the separation and splitting rules, or via performing inferences using our top-variable inference system combining with a form of dynamic renaming. Therefore, the problem of querying the (loosely) guarded fragment can be reduced to deciding the (loosely) guarded fragment and possibly irreducible query clauses, i.e., a clause that cannot derive any new conclusion. Meanwhile, our procedure yields a goal-oriented query rewriting algorithm: Before introducing datasets, one can produce a saturated clausal set $\mathcal{S}$ using given BCQs and (loosely) guarded theories. Clauses in $\mathcal{S}$ can be easily transformed first-order queries, therefore query answering over the (loosely) guarded fragment is reduced to evaluating a union of first-order queries over datasets. As far as we know, this is the first practical decision procedure for answering and rewriting Boolean conjunctive queries over the guarded fragment and the loosely guarded fragment.

cs.LO↗

arXiv2020

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 queries and cloud queries, which using our procedure, can be answered against the loosely guarded fragment.

cs.LO↗