The problem of answering Boolean conjunctive queries over the guarded fragment is decidable, however, as yet no practical decision procedure exists. In this paper, we present a resolution decision procedure to address this problem. In particular, we show that using the top-variable inference system, the separation rule and a form of dynamic renaming, one can derive a saturated set of query clauses and guarded clauses. As far as we know, this provides the first practical decision procedure for answering Boolean conjunctive queries over the guarded fragment.
of predicate symbols and the number of variables are limited. Also, guarded existential rules
can be seen as Horn guarded formulae. Querying GF is known to be 2ExpTime-complete [
One of the main challenges in this work is the handling of BCQs, since these formulae, e.g.,
∃( ∧ ), are beyond GF. By simply negating a BCQ, one can obtain a query clause: a
clause containing only negative literals in which only variables and constants are arguments,
such as ¬ ∨ ¬. One can take query clauses as (hyper-)graphs where variables are
vertices and literals are edges. Then we use a separation rule Sep [
Top variable resolution TRes is inspired by the ‘MAXVAR’ technique in deciding the loosely
guarded fragment [
Another task is building an inference system to reason with guarded clauses. Existing
inference systems for GF are either based on tableau (see [
Let C, F, P denote pairwise disjoint discrete sets of constant symbols , function symbols and predicate symbols , respectively. A term is either a variable or a constant or an expression (1, . . . , ) where is a -ary function symbol and 1, ..., are terms. A compound term is a term that is neither a variable nor a constant. A ground term is a term containing no variables. An atom is an expression (1, . . . , ), where is an -ary predicate symbol and 1, . . . , are terms. A literal is an atom (a positive literal) or a negated atom ¬ (a negative literal). The terms 1, . . . , in literal = (1, . . . , ) are the arguments of . A first-order clause is a multiset of literals, presenting a disjunction of literals. An expression can be a term, an atom, a literal, or a clause.
We use dep() to denote the depth of a term , formally defined as: if is a variable or a constant, then dep() = 0; and if is a compound term (1, . . . , ), then dep() = 1 + ({dep() | 1 ≤ ≤ }). In a first-order clause , the length of means the number of literals occurring in , denoted as len(), and the depth of means the deepest term depth in , denoted as dep(). Let , , , denote a sequence of variables, a set of variables, a set of atoms and a set of clauses, respectively. Let var(), var() be a set of variables in a an expression .
The rule set Σ denotes a set of first-order formulae and the database denotes a set of ground atoms. A Boolean conjunctive query (BCQ) is a first-order formula of the form ∃ () where is a conjunction of atoms, in which arguments are only constants and variables. Thus we can answer a Boolean conjunctive query Σ ∪ |= by checking the satisfiability of Σ ∪ ∪ ¬. In this work, we particularly focus on the case when Σ is expressed in GF without function symbols and equality.
In this section, we provide the formal definitions of GF and define a structural transformation so that guarded formulae and BCQs can be converted into suitable sets of clauses. Definition 1 (Guarded Fragment). Without equality and function symbols, the guarded fragment (GF) is a class of first-order formulae, inductively defined as follows: 1. ⊤ and ⊥ belong to . 2. If is an atom, then belongs to . 3. is closed under Boolean combinations. 4. Let belong to and an atom. Then ∀( → ) and ∃( ∧ ) belong to if all free variables of are among variables of . is referred to as guard.
Clausal Transformation. We now introduce the clausal transformation for GF and BCQs.
We use Q-Trans to denote our clausal transformation, which is a variation of the structural
transformation used in [
If an input formula is a BCQ, then we simply negate the BCQ to obtain a query clause. Using Q-Trans, a guarded formula can be transformed into a set of clauses as follows: 1. Add existential quantifiers for all free variables in and transform into negation normal form, obtaining the formula . 2. Apply the structural transformation: introduce fresh predicate symbols ∀ for universally quantified subformulae, obtaining . 3. Transform into prenex normal form and then apply Skolemisation, obtaining . 4. Drop all universal quantifiers and transform into conjunctive normal form, obtaining a set of guarded clauses.
We use the following notions to formally define query clauses and guarded clauses. A literal
is flat if each argument in it is either a constant or a variable. A literal is simple [
A query clause is a flat first-order clause containing only negative literals.
Definition 3. A guarded clause is a simple and covering first-order clause satisfying the following conditions:
2. contains a negative flat literal ¬ satisfying var() = var(). is referred to as guard.
In this section, we present the top variable based inference system from [
Let ≻ be a strict ordering, called a precedence, on the symbols in C, F and P. An ordering ≻ on expressions is liftable if 1 ≻ 2 implies 1 ≻ 2 for all expressions 1, 2 and all substitutions . An ordering ≻ on literals is admissible, if i) it is well-founded and total on ground literals, and liftable, ii) ¬ ≻ for all ground atoms , iii) if ≻ , then ≻ ¬ for all ground atoms and . A ground literal is (strictly) ≻ -maximal with respect to a ground clause if for any ′ in , ⪰ ′ ( ≻ ′). A non-ground literal is (strictly) maximal with respect to a non-ground clause if and only if there is a ground substitution such that is (strictly) maximal with respect to , that is, for all ′ in , ⪰ ′ ( ≻ ′ ). A selection function Select() selects a possibly empty set of occurrences of negative literals in a clause with no other restriction imposed. Inferences are only performed on eligible literals. A literal is eligible in a clause if either nothing is selected by the selection function Select() and is a ≻ -maximal literal with respect to , or is selected by Select().
The top variable based inference system T-Inf containing the rules: Deduct, Split, Fact, Res, TRes using the refinement T-Refine , given as follows.
∪ {} ∪ { ∨ } ∪ {} | ∪ {} ∨ 1 ∨ 2 ( ∨ 1) if is a conclusion of either Res, or TRes, or Fact, derived from clauses in . if and are non-empty and variable disjoint. if no literal is selected in , and 1 is maximal w.r.t.
∨ 1 ∨ 2. is an mgu of 1 and 2.
Res: ∨ 1 ¬ ∨
(1 ∨ ) if i) either is selected, or nothing is selected in ¬ ∨ and ¬ is the maximal literal, ii) is strictly ≻ -maximal w.r.t. 1. The premises are variable disjoint and is an mgu of and . 1 ∨ 1, . . . , ∨ , . . . , ∨ ¬1 ∨ . . . ∨ ¬ ∨ . . . ∨ ¬ ∨ (1 ∨ . . . ∨ ∨ ¬+1 ∨ . . . ∨ ¬ ∨ ) if i) there exists an mgu ′ such that ′ = ′ for each such that 1 ≤ ≤ , making ¬1 ∨ . . . ∨ ¬ top-variable literals and being selected, and is positive, iv) no literal is selected in 1, . . . , and 1, . . . , are strictly ≻ -maximal w.r.t. 1, . . . , , respectively. The premises are variable disjoint and is an mgu such that = for all such that 1 ≤ ≤ .
The top-variable literals are computed using ComputeTop(1, . . . , , ) in three steps: 1. Without producing or adding the resolvent, compute an mgu ′ among 1 = 1 ∨ 1, . . . , = ∨ and = ¬1 ∨ . . . ∨ ¬ ∨ such that ′ = ′ for each satisfying that 1 ≤ ≤ . 2. Compute the variable order > and = over variables in ¬1 ∨ . . . ∨ ¬: > if dep( ′) > dep( ′) and = if dep( ′) = dep( ′). 3. Based on > and =, identify the maximal variables in ¬1 ∨ . . . ∨ ¬, which we call the top variables. The top-variable literals for an application of TRes to are literals in containing at least one top variable.
We use T-Refine to denote the following resolution refinement: i) a lexicographic path
ordering ≻ [
Theorem 1 ([
We use the separation and splitting rules to ‘cut of’ branches of query clauses. A clause is indecomposable if it cannot be partitioned into two non-empty variable-disjoint subclauses. Using Split, a decomposable query clause can be transformed into a set of indecomposable query clauses. Hence from now on, we assume all query clauses are indecomposable.
Given a query clause , we use the notion of surface literal to divide variables in into two kinds of variables, i.e., chained variables and isolated variables. We say is a surface literal in a query clause if for any ′ in that is distinct from , var() ̸⊂ var(′). Let surface literals in a query clause be 1, . . . , where ≥ 1. Then the chained variables in are variables among ⋃︀ var() ∩ var( ) whenever var() ̸= var( ), i.e., variables that link ,∈ distinct surface literals containing non-inclusive variable sets, and isolated variables are the other non-chained variables. Now we can present the separation rule:
Sep:
∪ { ∨ ∨ } ∪ { ∨ ∨ (), ¬() ∨ } if i) is negative surface literal containing both chained variables and isolated variables , ii) ⊆ var() and ̸⊆ var(), iii) var() ⊆ var(), iv) is a definer .
Sep is a replacement rule in which the premise ∨ ∨ is immediately replaced by its conclusions ∨ ∨ () and ¬() ∨ . We say a query clause containing only chained variables is a chained-only query clause and a query clause containing only isolated variables is an isolated-only query clause. E.g., ¬(1, 2) ∨ ¬(2, 3) ∨ ¬(3, 4) ∨ ¬(4, 1) is a chained-only query clause where 1, 2, 3 and 4 are all chained variables, whereas ¬(1, 2, 3) ∨ ¬(2, 3) is an isolated-only query clause where 1, 2 and 3 are all isolated variables. According to the definition of chained variables, if a query clause contains no chained variables, then either contains only one surface literal, or all surface literals in share the same variables. Therefore Lemma 1. An indecomposable isolated-only query clause is a guarded clause.
Now we look at how Sep handles indecomposable query clauses.
Lemma 2. Exhaustively applying Sep to an indecomposable query clause transforms it into
So far we have considered how Sep handles query clauses. However, Sep itself is not suficient to handle chained-only query clauses such as ¬1 ∨ ¬2 ∨ ¬3, where there exists a so-called ‘variable cycle’ among , and . We employ the TRes rule to break such variable cycles while avoiding term depth increase in derived clauses.
Example 1. Given a chained-only query clause and a set of guarded clauses 1, . . . , 6: = ¬1 ∨ ¬2 ∨ ¬3 ∨ ¬1 ∨ ¬2 ∨ ¬3 1 = 1( , ) ∨ () ∨ ¬1 2 = 2( , ) ∨ ¬2 3 = 3(, ) ∨ ¬3 5 = 2( , ) ∨ ¬5 4 = 1( , ) ∨ ¬4 6 = 3(, ) ∨ ¬6 ComputeTop(, 1, . . . , 6) computes the mgu {/ ( ( (1, 1), ′), * ), / ( (1, 1), ′), / (1, 1), / ( (1, 1), ′), / (1, 1)} among and 1, . . . , 6. Hence is the only top variable in , so that TRes is performed on , 1 and 3, deriving = ¬1 ∨ ¬3 ∨ () ∨ ¬2 ∨ ¬1 ∨ ¬2 ∨ ¬3.
The first two figures in Figure 1 illustrate the variable relations of the flat literals in query clause and in TRes-resolvent of Example 1. A cycle among , and in is broken by TRes. The new challenge in this example is that is neither a guarded clause nor a query clause. On such resolvents we use the following structural transformation: we introduce fresh predicate symbols , and use ¬ to replace the literals that are introduced to the query Q: y
A1 x A2
A3 z B2
B1 w u B3
R: y G1, G3 x
A2 B2
B1 w u B3
Q1: y dt x
A2 B2
B1 w u B3
Q2: x B2
B1 w u B3 clause, so that is transformed into: ¬1 ∨ ¬3 ∨ () ∨ and ¬ ∨ ¬2 ∨ ¬1 ∨ ¬2 ∨ ¬3. The former is a guarded clause and the latter is a query clause.
We apply denote such structural transformation as T-Trans and apply it as the following manner: Let TRes derive the resolvent (¬+1 ∨ . . . ∨ ¬ ∨ 1 ∨ . . . ∨ ∨ ) using guarded clauses 1 ∨ 1, . . . , ∨ as the positive premises, a chained-only query clause = ¬1 ∨ . . . ∨ ¬ as the negative premise and a substitution such that = for all such that 1 ≤ ≤ as an mgu. Then T-Trans introduces fresh predicate symbols to transform into a set of clauses, in the following manner: Let 1, . . . , be top variables in . Then we partition 1, . . . , into sets 1, . . . , such that i) each pair of sets contain no common variable, and ii) each pair of variables in a set co-occurs in a literal of . Then for each set in 1, . . . , containing variables , if occur in , we introduce a definer for . Lemma 3. Let be a chained-only query clause and be a set of guarded clauses, T-Trans transforms TRes-resolvents of and (if TRes is applicable) into a set of guarded clauses and a query clause, of which the length is smaller than that of .
Using T-Trans, in Example 1 produces a query clause 1 = ¬ ∨ ¬2 ∨ ¬1 ∨ ¬2 ∨ ¬3 and a guarded clause ∨ ¬1 ∨ ¬3 ∨ () with a T-definer . The newly derived query clause 1 has branches, hence one can use Sep to cut the branch ¬ ∨ ¬2 from 1 by introducing a definer , obtaining a guarded clause ∨ ¬ ∨ ¬2 and a query clause 2 = ¬ ∨ ¬1 ∨ ¬2 ∨ ¬3, which is a chained-only query clause. Then one can break the cycle in 2 by TRes and derives a resolvent that can be 1 , ← 2 ← ∪ 3 if is a chained-only query clause then 4 return SaturateCOQC(, ) Algorithm 2: Saturation procedure of query clauses and guarded clauses Q-Saturate Input: A query clause , a set of guarded clauses
SepSplit() 10 5 else return SaturateGC( ∪ ); 6 7 Function SaturateCOQC(, ): 8 if is a guarded clause then return SaturateGC( ∪ ); 9 else if i) TRes is not applicable to and SaturateGC() or ii) all inferences between and SaturateGC() are redundant then
return SaturateGC() ∪ ← TRes(1, . . . , , ) ; , ′ ← T-Trans() ′, ′ ← SepSplit(′) ← ∪ ′ ∪ return SaturateCOQC(, ) ∪ SaturateCOQC(, ′)
◁ 1, . . . , ∈ SaturateGC() later renamed into guarded clauses using T-Trans. The last two figures in Figure 1 show the variable relations in 1 and 2 (the unary ¬ is omitted). We can see how Sep cut of 1’s branches.
Noticing that all the ‘byproducts’ of Sep, TRes and T-Trans are guarded clauses, we realise that, given a query clause , these rules only produce guarded clauses from . In fact, we found that the given query clause will eventually be reduced to either a guarded clause or chained-only query clauses. Algorithm 2 formally describe the procedure to saturate query clauses and guarded clause, namely Q-Saturate. SepSplit() is a function that recursively applies Sep and Split to a query clause , outputting guarded clauses , and either an isolated-only query clause (a guarded clause, Lemma 1) or a chained-only query clause . SaturateCOQC(, ) is a function that saturates guarded clauses and a chained-only query clause . SaturateGC() is a function that uses T-Inf system to saturate guarded clauses . TRes(1, . . . , , ) denotes a function that applies TRes to guarded clauses 1, . . . , and a chained-only query clause , and outputs the resolvent . T-Trans() is a function that applies T-Trans to the TRes-resolvent , deriving guarded clause and a query clause ′.
Since it is known that T-Inf decides guarded clauses [
Lemma 5. Sep and T-Trans only introduce a finitely bounded number of definers.
We can show that T-Inf combined with Q-Saturate is sound and refutationally complete. Theorem 2. Let be a set of clauses that is saturated up to redundancy with respect to T-Inf and Q-Saturate. Then, is unsatisfiable if and only if contains an empty clause. Theorem 3. Q-Saturate decides guarded clauses and query clauses. Together with the clausal transformation Q-Trans, Q-Saturate solves BCQ answering for GF.
In this paper, we present, as far as we know, the first practical query answering procedure
Q-Saturate that solves BCQ answering for GF. During the investigation, we found it interesting
that the same resolution-based techniques in automated reasoning are connected to techniques
found in the database literature. Since the mainstream query answering procedure in database
research uses a tableau-like chase approach [
We thank Uwe Waldmann and PAAR 2020 reviewers for the very useful comments. Sen Zheng’s work is partially sponsored by the Great Britain-China Educational Trust.