Most Description Logics (DLs) can be translated into wellknown decidable fragments of rst-order logic FO, including the guarded fragment GF and the two-variable fragment FO2. Given their prominence in DL research, we take closer look at GF and FO2, and present a new fragment that subsumes both. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard de nition of GF: quanti cation is required to be guarded only for subformulae with three or more free variables. We show that satis ability of equality-free TGF is N2ExpTime-complete, but becomes NExpTime-complete if we bound the arity of predicates by a constant (a natural assumption in the context of DLs). Finally, we observe that many natural extensions of TGF, including the addition of equality, lead to undecidability.
Description Logics (DLs) are a family of logic-based knowledge representation
languages, usually suitably limited to ensure the decidability of basic reasoning
problems [
An alternative explanation for the decidability of DLs is the fact that they
can often be translated into the guarded fragment GF of FO [
Given the importance of GF and FO2 to research in DLs, in this paper we take a deeper look at them, and study a new fragment of FO that subsumes both GF and FO2. The fragment is called the triguarded fragment (denoted TGF), and it is obtained by relaxing the standard de nition of GF. In GF, existential and universal quanti cation can only be used in (sub)formulae of the form 9x:(R(t) ^ ) or 8x:(R(t) ! ), where R(t) is an atomic formula such that t contains all free variables of (the atom R(t) \guards" the formula ). In TGF, guardedness of quanti cation is required only in case has three or more free variables (hence the name \triguarded"). This entails that quanti cation can be used in an unrestricted way for formulae with at most two free variables, and hence FO2 gets included in TGF seamlessly.
After providing a simple de nition of TGF, we study its satis ability problem. To this end, we rst consider a slightly di erent problem: we study satis ability of formulae of GF in the presence of a built-in binary predicate U that contains all pairs of domain elements. In DL parlance, we consider the extension of GF with the universal role, and thus this fragment is denoted GFU. Since the predicate U can be used to provide \spurious" guards to formulae with up to two free variables, GFU adds to GF precisely the expressivity needed to capture TGF, and thus in the paper we mainly focus on GFU instead of TGF.
We show that in the equality-free case, satis ability of formulae in GFU (and in TGF) is N2ExpTime-complete. We establish the upper bound by characterizing the satis ability of a formula in GFU via mosaics, where a mosaic is a special ( nite) collection of types that can be used to build a model for the input formula. The matching lower bound can be obtained by a reduction from the tiling problem of a doubly exponential grid. We then consider the assumption that predicate arities are bounded by a constant. In this case, the mosaic construction gives rise to a NExpTime upper bound for satis ability of formulae without equality. We note that FO2 is already NExpTime-hard (even without equality), which means that in the bounded-arity setting TGF and GFU do not have higher complexity than FO2. Finally, we show that satis ability of TGF and GFU formulae with equality is undecidable (interestingly, the complexity of satis ability in GF and FO2 is insensitive to the presence of equality).
The fragment GFU is similar to the fragment GF 2 of [
We assume the reader is familiar with the syntax and semantics of FO, and thus here we only present some notation. We use NP, NC and NV to denote the countably in nite, mutually disjoint sets of predicate symbols, constants and variables, respectively. We will mostly use (possibly subscripted) P , R, B and H as predicate symbols. Given a formula ', we use NC(') and NP(') to denote the set of constants and the set of predicate symbols that appear in ', respectively. Elements of NC [ NV are called terms. An atom (or, atomic formula) is an expression of the form R(t), where t is an n-tuple of terms, where n is the arity of the predicate symbol R 2 NP. For convenience, given a tuple t = ht1; : : : ; tni of terms, we sometimes view t as the set ft1; : : : ; tng. Given a tuple x of variables, an x-assignment is any function f : NC [ NV ! NC [ NV such that (i) f (y) 2 NC for all y 2 x, and (ii) f (t) = t for all t 62 x. Given a tuple t = ht1; : : : ; tni of terms and an x-assignment f , we let f (t) = hf (t1); : : : ; f (tn)i. The semantics to formulae is given using interpretations. An interpretation is a pair I = ( I ; I ), where I is a non-empty set (called domain), and I is a function that maps (i) every constant c 2 NC to an element cI 2 I , and (ii) every predicate symbol R 2 NP to an n-ary relation over I , where n is the arity of R. We assume that 0-ary predicate symbols > and ? belong to NP, and they have the usual (built-in) meaning. The equality predicate also belongs to NP, and has the xed meaning I = f(e; e) j e 2 I g for all interpretations I. We write I j= ', if an interpretation I is a model of a closed formula (or, a sentence) '. We use free(') to denote the set of free variables in a formula '. 3
We are now ready to introduce the triguarded fragment of FO. Essentially, it is a relaxed variant of GF where guards are only required when quantifying over formulae with three or more free variables.
De nition 1. The triguarded fragment TGF of rst-order logic with equality is de ned as the smallest set of formulae closed under the following rules: (1) Every atomic formula belongs to TGF. (2) TGF is closed under the propositional connectives :, ^, _ and !. (3) If x is a variable, and ' is a formula in TGF with jfree(')j 2, then 9x:' and 8x:' also belong to TGF. (4) If x is a non-empty tuple of variables, ' is a formula in TGF, is an atom, and free(') free( ), then 9x:( ^ ') and 8x:( ! ') also belong to TGF.
Observe that if we consider only the items (1), (2) and (3) in De nition 1 as legal rules to build formulae, we can build all formulae of FO that use at most 2 variables, and thus FO2 TGF. If we consider the items (1), (2) and (4) in De nition 1, we can build all guarded formulae, and thus GF TGF. The syntax of TGF also allows us to build formulae that are neither in GF nor in FO2, witnessed by formulae like
8x8y:((R1(x; a) ^ R2(y; b)) ! 9z:R3(x; y; z)): Our main goal in this paper is to understand the computational complexity of satis ability in TGF. To this end, we concentrate on a slightly di erent logic, which is e ectively equivalent to TGF, but which makes presentation signi cantly easier. In particular, there is a simple extension of GF that allows us to capture TGF. Intuitively, TGF 6 GF because TGF allows \unguarded" quanti cation in front of formulae ', but only in case ' has no more than 2 free variables. If we have the availability of a binary predicate whose extension always contains all pairs of domain elements, we can use it to guard '. In particular, we consider next the binary universal role predicate U 2 NP, whose extension is xed to be UI = I I for all interpretations I. Note that in FO, FO2 and TGF, the built-in predicate U does not add expressiveness, because it can be axiomatized using an ordinary binary predicate U and the sentence = 8x8y:U (x; y); thus we can safely allow U to be used as a predicate symbol in formulae of FO, FO2 and TGF. Since is not in GF, the addition of the built-in U to GF makes a big di erence (as we shall see from complexity results). We now formally de ne GFU, which extends GF with U, and in fact adds to GF the necessary expressivity to capture TGF.
De nition 2. Let GFU be the set of formulae of TGF that can be built using the items (1), (2) and (4) of De nition 1 only, possibly using the predicate U in atomic formulae.
By using the U predicate as a guard for formulae with at most 2 free variables, we can convert any TGF formula into an equivalent formula in GFU. For instance, the above example formula can be transformed into the equivalent GFU formula 8x8y:(U(x; y) ! ((R1(x; a) ^ R2(y; b)) ! 9z:R3(x; y; z))): Proposition 1. For any ' 2 TGF, we can build in polynomial time an equivalent formula '0 2 GFU. Moreover, NP('0) NP(') [ fUg.
Due to Proposition 1, in order to check satis ability in TGF, it su ces to focus on the satis ability problem for GFU, and thus in the rest of the paper we focus on GFU. 4
In this section, we study GFU in the equality-free setting, and provide a nite representation of models of satis able GFU formulae, which will be the basis of the satis ability checking algorithm. In particular, we show that an equality-free GFU formula ' has a model i there exists a mosaic for ', which is a relatively small set of building blocks that can be used to build a model for '. In this way, checking satis ability of ' reduces to checking the existence of a mosaic for '.
To simplify the structure of GFU formulae we use a suitable (Scott-like)
normal form, which is not much di erent from the ones used, e.g., in [
As usual, in case m = 0, the empty disjunction in (1) stands for ?. Note that since (1) and (2) are in GFU, each variable that appears in v1; : : : ; vm also appears in t, and each variable that appears in v also appears in u. Observe that the sentence in (1) can be equivalently written as 8x:(R(t) ^ H(v1) ^ : : : ^ Hn(vn) ! Hn+1(vn+1) _ : : : _ Hm(vm)): (3) For presentation reasons, in what follows we will mostly use the form (3) instead of (1) when speaking about sentences in A. Note that (3) closely resembles a (guarded) disjunctive Datalog rule with R(t) a guard atom.
The following statement shows that we can focus on formulae in normal form. Proposition 2. For any formula ' 2 GFU, we can construct in polynomial time a formula '0 2 GFU in normal form such that (a) ' is satis able i '0 is satis able, and (b) the translation does not increase the arity of predicate symbols, i.e., there is no predicate symbol in '0 whose arity is strictly greater than the arity of every predicate symbol in '.
To de ne mosaics, we need the notion of a type for a formula '. Types will form mosaics, and they can be seen as patterns (interpretations of restricted size) for building models of '.
De nition 4 (Types). A type for a formula ' is any set of ground atoms with predicate symbols from NP('). We let dom( ) denote the set of constants that appear in a type , and let I( ) denote the interpretation such that (i)
I( ) = dom( ), and (ii) P I( ) = ft j P (t) 2 g for all predicate symbols P . For a sentence ', we write j= ' if I( ) j= '. Given a set of constants F , we let jF = fP (t) 2 j t F g, i.e., jF is the restriction of to atoms whose all arguments are included in F .
Of particular interest in our treatment is how a distinguished element of some type \looks like" in terms of the predicates it satis es and its relationship to constants. This information is captured using unary types, in which we abstract from the concrete target constant by replacing it with a special variable. De nition 5 (unary types). Assume a formula ' 2 GFU and let x' be a special variable associated with '. We let base(') denote the set of all atoms P (t) such that t NC(') [ fx'g and P 2 NP('). Any subset base(') is called a unary type for '. Assume a constant c, and let f be the function such that (i) f (x') = c, and (ii) f (d) = d for all d 2 NC. For a type , we de ne the unary type jc' = fR(t) 2 base(') j R(f (t)) 2 g.
We are now ready to de ne mosaics, which will act as witnesses to satis ability of GFU formulae (without equality). Roughly, a mosaic for a formula ' is a pair (M; X ), where X is a collection of \placeholder" constants, and M is a set of types for '. In order to be a proper witness to satis ability, a mosaic must satisfy a collection of conditions. In particular, they ensure that in case ' is satis able, we will be able to construct a model by arranging together (possibly multiple) instances of types from M. Intuitively, by an instance of a type 2 M we mean a concrete structure that is obtained by replacing the placeholder constants from X with concrete domain elements.
De nition 6 (Mosaic). A mosaic for a sentence ' 2 GFU in normal form is a pair (M; X ), where M is a set of types for ' and X NC n NC('), satisfying the following: (A) jX j (B) For all width('); 2 M, dom( )
NC(') [ X ; (C) For all ; 0 2 M, jNC(') = 0jNC('); (D) U(t; v) 2 for all
2 M and each pair t; v 2 dom( ); (E) j= for all 2 M and all 2 A('); (F) If 2 M, 8x:(R(t) ! 9y:H(v)) 2 E('), and R(g(t)) 2 assignment g, then there is some 0 2 M such that: (a) H(h(g(v))) 2 0 for some y-assignment h; (b) jF = 0jF , where F = NC(') [ fg(x) j x 2 x \ vg. for some x(G) If t1 2 dom( 1) \ X and t2 2 dom( 2) \ X for some 1; 2 2 M, then there exists a type 2 M and a pair v1; v2 with dom( ) \ X = fv1; v2g such that (i) v1 6= v2, (ii) 1jt'1 = jv'1 , (iii) 2jt'2 = jv'2 .
Intuitively, the conditions (A-G) ensure the following. (A) requires that only a small number of placeholder constants is used. Due to (B), types in mosaics only refer to original constants of the formula and the small number of place holder constants. The conditions (A) and (B) are important to ensure the relatively small size of mosaics. The condition (C) forces the types to agree on the participation of constants in predicates. (D) requires U to be correctly interpreted locally (i.e., within the individual types), and (E) requires each type to (locally) satisfy all sentences from A('). The condition (F) ensures that for each type locally satisfying the body of some sentence from E('), we nd a matching type where also the head of that sentence is satis ed. Using (G) we make sure that any two representatives of unnamed domain elements (in terms of unary types) found across the types also occur together in one type.
The following soundness and completeness theorems show that mosaics properly characterize satis ability of equality-free GFU formulae (and, due to Proposition 1, of equality-free TGF formulae).
Theorem 1 (Completeness). Let ' 2 GFU be a formula in normal form. If ' is satis able, then there exists a mosaic (M; X ) for '.
Proof (Sketch). Assume that ' has some model J . Since ' is equality-free, we can make the standard name assumption (SNA): NC(') J and cI = c for all c 2 NC('). Now, let I be obtained from J by duplicating all anonymous individuals. Formally, let anon = J n NC(') and I = NC(') [ f1; 2g anon. Let : I ! J such that (c) = c for c 2 NC(') and ((i; e)) = e otherwise.
Now we let t 2 P I if (t) 2 P J . As ' does not contain equality, J j= ' implies I j= '. This duplication of anonymous individuals makes sure that for every non-constant domain element e, I contains a twin element e~ di erent from e but with the same unary type. This property turns out to be crucial to show part (G) of the mosaic de nition.
We show how to extract from I a mosaic (M; X ) for '. We can assume, w.l.o.g., that I NC and that cI = c for all c 2 NC(').
Let X be any set with X NC, X \ I = ;, and jX j = width('). We say a type can be extracted from I if can be obtained from I in 4 steps: (a) Take any S I such that NC(') S and jSj jNC(')j width('). (b) Let = fP (t) j t S ^ t 2 P I g. (c) Let f be any injective function from dom( ) n NC(') to X . (d) Let be the type obtained from by replacing every occurrence of c 2 dom( ) n NC(') by f (c).
The set M contains all types that can be extracted from I. It is not di cult to see that the constructed (M; X ) is a mosaic for '. tu Theorem 2 (Soundness). Let ' 2 GFU be a formula in normal form. If there exists a mosaic (M; X ) for ', then ' is satis able.
Proof (Sketch). Assume a mosaic (M; X ) for '. An instantiation for a type 2 M is any injective function from dom( ) \ X to NC n X . Given such and , we use ( ) to denote the type that is obtained from by replacing every occurrence of a constant c 2 dom( ) \ X by (c). Our goal is to show how to inductively construct a possibly in nite sequence S = ( 0; 0); ( 1; 1); : : : of pairs ( j ; j ), where j 2 M and j is an instantiation for j , such that Si 0 i( i) j= '.
In the base case, we let 0 be an arbitrary type from instantiation for 0.
M, and let 0 be any
For the inductive case, suppose ( 0; 0); : : : ; ( i 1; i 1) have been de ned, where i > 0. We show how de ne the next segment ( i; i); : : : ; ( m; m) of S, where m i (we indeed may attach to S multiple new elements in one step). To this end, choose the smallest index 0 j i 1 satisfying the following condition: there is 8x:(R(t) ! 9y:H(v)) 2 E('), and R(g(t)) 2 j( j) for some x-assignment g. If such j does not exist, the construction of S is complete, and we can proceed to (?) below, where we argue that S0 k<i k( k) j= '. We assume that the above j exists. We rst show in (y) how to de ne ( i; i), and then in (z) how to de ne the remaining ( i+1; i+1); : : : ; ( m; m).
(y) From the x-assignment g construct the following x-assignment h. For every x 2 x, (i) let h(x) = g(x), if g(x) 2 dom( j), and (ii) let h(x) = j (g(x)), if g(x) 62 dom( j). Since R(g(t)) 2 j( j), we get R(h(t)) 2 j. Since the condition (F) is satis ed by the mosaic, there exists a type 0 2 M such that 1. H(f (g((v))) 2 0 for some y-assignment f ; 2. jF = 0jF , where F = NC(') [ fg(x) j x 2 x \ vg.
We let i = 0, and de ne an injective function i from dom( i) \ X to NC n X as follows. For every c 2 dom( i) \ X , we let i(c) = j(c) in case c 2 fh(x) j x 2 x \ vg, and otherwise we let i(c) be a fresh constant, i.e., a constant that does not appear in NC(') or in the range of any instantiation built so far.
(z) Let N be the set of all constants that were freshly introduced in S by i, i.e., N is the set of all i(c) such that c 2 dom( i) \ X but c 62 fh(x) j x 2 x \ vg. Intuitively, in order to properly deal with the U predicate, we need to nd in M proper types to connect every c 2 N with the relevant remaining constants of the sequence S constructed so far. Let (d1; d01); : : : ; (dn; d0n) be an enumeration of all pairs (d; d0) such that d 2 N and d0 2 S0 k i 1 ran( k), i.e. d0 is any constant that appears in the sequence S constructed so far but d0 62 N [ NC('). The de nition of the segment ( i+1; i+1); : : : ; ( m; m) of S in this inductive step is as follows. We let m = i + n, and for each 1 k n, we select ( i+1+k; i+1+k) as described next.
Assume an arbitrary 1 k n. We let c = i (dk), and let = l for some 0 l i such that d0k 2 ran( l). Let c0 = l (d0k). Due to Condition (G) in the de nition of mosaics, there exists a type 2 M such that (i) dom( ) \ X = fv1; v2g for some v1; v2 with v1 6= v2, (ii) ijc' = jv'1 , and (iii) jc'0 = jv'2 . Then we set i+1+k = , and let i+1+k = f(v1; dk); (v2; d0k)g.
(?) The above completes the construction of a candidate model for '. It is not too di cult to see that Si 0 i( i) j= '. tu 5
Using the characterization of the previous section, we can infer worst-case optimal upper bounds for satis ability checking in GFU, and thus in TGF. Theorem 3. Deciding satis ability of TGF and of GFU formulae without equality is N2ExpTime-complete. The problem is NExpTime-complete under the assumption that predicate arities are bounded by a constant.
Proof (Sketch). Due to Propositions 1 and 2, it su ces to show the two upper bounds for GFU formulae in normal form. Due to Theorems 1 and 2, we can decide the satis ability of a formula ' 2 GFU in normal form by checking the existence of a mosaic for '. Our approach is to non-deterministically guess a pair (M; X ) of a set M of types over NP(') together with a set of constants X of cardinality at most width('), and then verify that (M; X ) is indeed a mosaic for '. Note that given a candidate (M; X ) as input we can check in polynomial time whether (M; X ) satis es all the conditions given in De nition 6. Observe that the number of ground atoms over the signature of ' with arguments from NC(') [ X is bounded by jNP(')j (jNC(')j + width('))k, where k the maximal arity of predicates in '. Consequently, we can restrict ourselves to candidates (M; X ), where M has no more than 2jNP(')j (jNC(')j+width('))k types. Since this bound is double exponential in the size of ', but only single exponential under the assumption that k is a constant, the two upper bounds follow.
The matching lower bound for the bounded arity follows from the complexity
of FO2 [
In the presence of equality, we can show the undecidability of satis ability of GFU
(and hence of TGF) by a reduction from the tiling problem for an in nite grid
[
In the following, we omit leading universal quanti ers; all formulae are sentences. We start our modeling by ensuring there is exactly one leftmost, bottommost position of the grid, i.e., the \origin".
9x:Orig (x) U(x; y) ^ Orig (x) ^ Orig (y) ! x y Any two domain elements co-occur together with the origin in a ternary auxiliary predicate ChkFunc.
U(x; y) ! 9z:ChkFunc(x; y; z) ^ Orig (z) Intuitively, ChkFunc(x; y; z) indicates that we will enforce that if z is connected with both x and y by predicate V (or H ), then x and y must coincide; in other words, as x and y are arbitrary elements, z has only one outgoing V -connection and one outgoing H -connection. The following two sentences implement this.
ChkFunc(x; y; z) ^ H (z; x) ^ H (z; y) ! x
ChkFunc(x; y; z) ^ V (z; x) ^ V (z; y) ! x
y
y
1 As mentioned in the introduction, this undecidability result can be inferred from the
undecidability of the Goldfarb class, using the reduction in [
ChkFunc(x; y; z) ! 9w:ChkFunc(x; y; w) ^ H (z; w)
ChkFunc(x; y; z) ! 9w:ChkFunc(x; y; w) ^ V (z; w) With these axioms alone, the corresponding universal model would resemble an in nite binary tree, with the origin as root and every node having (exactly) one H -successor and (exactly) one V -successor. The next axioms make sure that for every element e in our structure, the element reached from e via an H -V -path coincides with the element reached from e via a V -H -path, using another auxiliary 5-ary predicate ChkSq which is handled in a way that ChkSq(x; y; z1; z2; z3) is only entailed whenever z1 has z2 as right neighbor and z3 as upper neighbor.
Again, we start ensuring this for e being the origin and then work our way through the structure along the (unique) H - and V - connections.
U(x; y) ! 9z1z2z3:ChkSq(x; y; z1; z2; z3) ^ Orig(z1) ^ H (z1; z2) ^ V (z1; z3) ChkSq(x; y; z1; z2; z3) ! 9w1w2:ChkSq(x; y; z2; w1; w2) ^ H (z2; w1) ^ V (z2; w2) ChkSq(x; y; z1; z2; z3) ! 9w1w2:ChkSq(x; y; z3; w1; w2) ^ H (z3; w1) ^ V (z3; w2) Finally, we ensure that if ChkSq(x; y; z1; z2; z3) holds and x is the right neighbor of z2 and y is the upper neighbor of z3, that then x and y must coincide.
ChkSq(x; y; z1; z2; z3) ^ V (z2; x) ^ H (z3; y) ! x y This nishes our modeling of the in nite grid. It is now straightforward to model a tiling on top of this, and we obtain the following theorem.
Theorem 4. Checking satis ability of TGF formuale with equality is undecidable. The same applies to GFU formulae with equality. 7
In this section, we will review further natural extensions of TGF and nd that they lead to undecidability.
Relaxing guardedness further. Unguarded quanti cation of subformulae with
three variables would allow to express any formula of the three-variable fragment
of FO, denoted FO3, for which satis ability is undecidable (as FO3 contains the
class of FO sentences with quanti er pre x 898 which is undecidable [
Loose guardedness. It has been shown that GF remains decidable if the
guardedness restriction is relaxed, leading to notions such as the loosely guarded
fragment, the packed fragment or the clique-guarded fragment. For most restrictive
notion of those, the loosely guarded fragment [
In this paper, we have introduced the triguarded fragment of FO which subsumes both GF and FO2. We clari ed the computational complexity of satis ability checking in this fragment, both for the bounded and unbounded arity case. We discussed that diverse natural extensions of the fragment lead to undecidability.
While both GF [
We thank Emanuel Kieronski and the anonymous reviewers for the valuable
comments. We are also grateful to Pierre Bourhis, Michael Morak, and Andreas
Pieris for clarifying some questions regarding their paper [
Sebastian Rudolph has been supported by the Institute of Logic and Computation (E192) at TU Wien and the ERC Consolidator Grant DeciGUT. Mantas Simkus has been supported by the Austrian Science Fund (FWF) projects P30360 and P30873.