Nominals for Everyone

1 Introduction

Description logics [Baader et al., 2003a], which have evolved from classical modal logic, are the core knowledge representation formalism of the semantic web as well as of many stand-alone ontologies. A key feature of many description logics is support for nominals, i.e., names for individuals to be used within concepts, rather than only in a separate collection of assertions about individuals, the ABox. Nominals allow in particular for a direct combination of knowledge about individuals with terminological knowledge.

Another group of features which is often recognised as desirable, but is not currently included in standard description logics, is formed by reasoning paradigms which go beyond the standard relational perspective. The latter is the semantic basis e.g. of existential or universal restrictions ∃R.C / ∀R.C along roles asserting that some or all R-successors, respectively, of an individual satisfy a concept C, and of the more general qualified number restrictions ≥nR.C / ≤nR.C which give explicit numerical bounds on the number of R-successors satisfying C. Features not supported by purely relational models include, e.g., reasoning with uncertainty, default implication, coalitional reasoning, or notions

∗Work of the first author forms part of the DFG project Generic Algorithms and Complexity Bounds in Coalgebraic Modal Logic (SCHR 1118/5-1). Work of the second author partially supported by EPSRC grant EP/F031173/1

Dirk Pattinson Clemens Kupke

Imperial College London dirk@doc.ic.ac.uk ckupke@doc.ic.ac.uk

of agency. There has been some interest in adding such features to description logics; see, e.g., the overview in Baader et al. [2003b] and the more recent survey by Lukasiewicz and Straccia [2008]. Some of these logics support nominals, e.g., Lukasiewicz's P-SHOIN(D) [2008]. A common feature of existing approaches is that they typically add a new reasoning principle only at the outermost level, e.g., by replacing concept inclusions in the TBox with conditional probabilities.

The generic framework of coalgebraic hybrid logic [Myers et al., 2009] integrates the basic features of hybrid logic - nominals and the satisfaction operator - with a wide variety of reasoning principles including, e.g., probability and other notions of uncertainty, non-monotonic conditionals, and reasoning about the power of coalitions. The new reasoning principles are embodied as modal operators and hence can be applied in a nested fashion. Their semantics often goes far beyond standard relational semantics, being based, e.g., on probabilistic structures, selection function models, or game frames. The common umbrella for all these structures is a coalgebraic semantics.

The main contribution of the present work is to promote coalgebraic hybrid logic to a full description logic by providing reasoning support for general TBoxes. Technically, we prove that under natural assumptions on the axiomatisation of the reasoning principles used in the logic at hand, in fact the same assumptions as previously used to establish a generic upper bound PSPACE for various purely modal logics [Schr¨oder and Pattinson, 2009], concept satisfiability over general TBoxes is in EXPTIME, typically a tight upper bound. We achieve this by first reducing the satisfiability problem to the existence of tableaux, and, in a second step, to the existence of winning strategies in parity games. Instantiation of the generic EXPTIME bound to particular logics yields, to our knowledge, new results in all non-relational cases, including the probabilistic case.

We conclude with a discussion of how our framework may be applied in ontological reasoning. We exploit in particular that coalgebraic semantics is modular [Schr¨oder and Pattinson, 2007] and hence allows for flexibly taylored combinations of reasoning principles and algorithms. We illustrate this point using different combinations of probabilistic and relational semantics in an ontology of the Tudor dynasty.

2 Nominals in Coalgebraic Logic

We recall the generic framework of coalgebraic hybrid logic [Myers et al., 2009]. It covers a range of logics that feature modal operators interpreted over a wide variety of system types, nominals designating individuals within a system, and satisfaction operators that permit to assert properties of individuals at any place within a formula, thus in particular allowing for internalisation of ABoxes.

The framework is parametric in both syntax and semantics. The syntax of a given logic is determined by a (modal) similarity type Λ consisting of modal operators with associated arities, which we fix throughout. For given countably infinite and disjoint sets P of propositional variables and N of nominals, the set F(Λ) of hybrid Λ-formulas is given by the grammar

where p ∈ P, i ∈ N and ♥ ∈ Λ is an n-ary modal operator. We use the standard definitions for the other propositional operators →,↔, ∨,⊤,⊥. The set of nominals occurring in a formula φ is denoted by N(φ). A formula of the form @iφ is called an @-formula. For Σ ⊆ F(Λ),we put N(Σ) = ⋃φ∈Σ N(φ) and @Σ = {φ ∈ Σ | φ @-formula}. Semantically, nominals i denote individual points in a model, and an @-formula @iφ stipulates that φ holds at i.

The parametrisation of the semantics is essentially the standard coalgebraic semantics of modal logics. In particular, the type of systems underlying the semantics is determined by the choice of an endofunctor T : Set → Set on the category of sets, to be thought of informally as a parametrised datatype (formally, T maps sets X to sets TX and maps X → Y to maps TX → TY , compatibly with identities and composition). Then, T-coalgebras play the roles of frames. A T-coalgebra is a pair (C, γ) where C is a set of states (or individuals) and γ : C → TC is the transition function. When γ is clear from the context, we identify a T-coalgebra (C, γ) with its state space C.

• Example 2.1. 1. The (covariant) powerset functor P maps a set X to its powerset P(X); its coalgebras C → P(C) are in bijection with Kripke frames (C, R ⊆ C × C).
• The multiset functor B maps a set X to the set of multisets overX, i.e., mapsX → ∪{∞} assigningmultiplicities to elements of X. Its coalgebras are multigraphs, a variant of Kripke frames where edges are annotated with positive integer multiplicities [D'Agostino and Visser, 2002].
• The distribution functor D maps a set X to the set of finitely supported probability distributions on X; its coalgebras are Markov chains, also variously referred to as probabilistic type spaces [Heifetz and Mongin, 2001] or probabilistic transition systems.
• Coalgebras for the functor CF taking a set X to the set P(X) → P(X) of selection functions over X are precisely conditional frames [Chellas, 1980], also called selection function models.
• Coalgebras for the functor Gn taking a set X to the set {(S1, ..., Sn, f) | S1, ..., Sn nonempty sets (of strategies), f : (∏ Si) → X} of n-player strategic games over X are Pauly's game frames [2002].

The interpretation of an n-ary modal operator ♥ ∈ Λ is given by an n-ary predicate lifting [[♥]], i.e., a family of maps [[♥]]X : P(X)n → P(TX), indexed over all sets X, such that

The semantics induced by these parameters, which we fix throughout, is a satisfaction relation |= between states c ∈ C in (hybrid) T-models M = (C, γ, π) and formulas φ ∈ F(Λ). Here, M consists of a T-coalgebra (C, γ) and a hybrid valuation π, i.e., a map P ∪ N → P(C) that assigns singleton sets to all nominals i ∈ N, where we often identify the singleton set π(i) with its unique element. Satisfaction is inductively defined by the obvious clauses for the propositional part, and by

where x ∈ N∪P, i ∈ N, ♥ ∈ Λ n-ary, and [[φ]]M = {c ∈ C | c,M |= φ}. The focus of the present work is on reasoning over so-called general TBoxes: Given a set Γ ⊆ F(Λ) of global assumptions, the TBox, we say that M is a Γ-model if c,M |= φ for all c ∈ C and all φ ∈ Γ. A formula φ (a set Φ of formulas) is Γ-satisfiable if there exists a state satisfying φ (all formulas in Φ) in some Γ-model. Note that thanks to the satisfaction operator, an ABox, i.e., a set of assertions about individuals, may be encoded either in the formula φ itself or in the TBox Γ.

Example 2.2. We recall a few basic examples that use the functors from Example 2.1.

1. The hybrid version of the modal logic K, hybrid K for short, has a single unary modal operator ✷, interpreted over the powerset functor P by [[✷]]X(A) = {B ∈ P(X) | B ⊆ A}. This coalgebraic definition of satisfaction translates to the usual semantics of the box operator along the bijection between P-coalgebras and Kripke frames, inducing the standard semantics of hybrid logic [Areces and ten Cate, 2007]. The description logic ALCO is a notational variant of a sublogic of multi-agent hybrid K (captured coalgebraically using multiple copies of the powerset functor).
2. Graded hybrid logic has modal operators ✸k 'in more than k successors, it holds that'. It is interpreted over the multiset functor B by [[✸k]]X (A) = {B ∈ B(X) | ∑x∈A B(x) > k}. This captures the semantics of graded modalities over multigraphs [D'Agostino and Visser, 2002]. One can encode the description logic ALCOQ (which features qualified number restrictions ≥nR and has a relational semantics) into multi-agent graded hybrid logic with multigraph semantics by adding formulas ¬✸1i for all occurring nominals i to the TBox.
3. Probabilistic hybrid logic, the hybrid extension of probabilistic modal logic [Larsen and Skou, 1991; Heifetz and Mongin, 2001], has modal operators Lp 'in the next step, it holds with probability at least p that', for p ∈ [0, 1] ∩ . It is interpreted over the distribution functor D by putting [[Lp]]X (A) = {P ∈ D(X) | PA ≥ p}.

1. Hybrid CK, the hybrid extension of the basic conditional logic CK, has a single binary modal operator ⇒, written in infix notation and read, e.g., as a non-monotonic default implication. Hybrid CK is interpreted over the functor CF by putting [[⇒]]X (A,B) = {f : P(X) → P(X) | f(A) ⊆ B}. Other conditional logics with additional axioms, e.g., cautious monotony, are captured similarly. As a simple example, the fact that the national football championship is typically won by team i (an observation that fits a number of countries) is expressed in hybrid conditional logics by the formula champion ⇒ i.

5. Hybrid coalition logic, the hybrid version of Pauly's coalition logic [2002], has modal operators [C] 'the coalition C ⊆ {1, ..., n} of agents can force . . . '. These are interpreted by suitable predicate liftings for the functor Gn [Schr¨oder and Pattinson, 2009]. Given a Gn-coalgebra (C, γ), C is the set of states in a strategic game, and nominals therefore encode individual positions.

Our generic complexity result will be based on axiomatisations in a certain format; we require the following notation.

Definition 2.3. The set of boolean combinations over a set V is denoted Prop(V ). A clause over a set V is a disjunction of literals over V , i.e., elements of V ∪ {¬v | v ∈ V }. The set of clauses over V is denoted Cl(V ). A conjunctive normal form (CNF) of φ ∈ Prop(V ) is a subset of Cl(V ) whose disjunction is propositionally equivalent to φ. For Φ ⊆ Prop(V ), ψ ∈ Prop(V ), we write Φ ⊢PL ψ ('Φ propositionally entails ψ') if there exist φn, ..., φn ∈ Φ such that φ1 ∧ ... ∧ φn → ψ is a propositional tautology. A valuation τ : V → P(X) for some set X induces in the obvious way an interpretation [[φ]]τ ⊆ X. Moreover, we put Λ(X) = {♥(x1, ..., xn) | ♥ ∈ Λ n-ary, x1, ..., xn ∈ X}. Given τ as above, one obtains for φ ∈ Prop(Λ(Prop(V ))) a one-step semantics [[φ]] ⊆ TX extending the assignment [[♥(φ1, ..., φn)]]τ = [[♥]]X ([[φ1]]τ, ..., [[φn]]τ).

Using these notions, we can now define the crucial prerequisites for the generic reasoning algorithm.

Definition 2.4. A (one-step) rule R = φ/ψ over a set V of propositional variables consists of a premise φ ∈ Prop(V ) and a conclusion ψ ∈ Cl(Λ(V )). The rule R is one-step sound if whenever [[φ]]τ = X for a valuation τ : V → P(X), then [[ψ]]τ = TX. A set R of one-step rules is strictly one-step complete if whenever [[χ]]τ = TX for some τ : V → P(X) and some χ ∈ Cl(Λ(V )), then there exist a rule φ/ψ ∈ RC and a V -substitution σ such that ψσ ⊢PL χ and X, τ |= φσ. Here, RC denotes the extension of R with congruence rules a1 ↔ b1; ...; an ↔ bn/♥(a1, ..., an) ↔ ♥(b1, ..., bn) for ♥ ∈ Λ n-ary.

Strict one-step completeness essentially amounts to absorption of cut by the rule system. Strictly one-step complete rule sets for the logics of Example 2.2 are given in [Schr¨oder and Pattinson, 2009; Pattinson and Schr¨oder, 2008]. E.g., for hybrid K, the set of rules a1 ∧ ... ∧ an → b/✷a1 ∧ ... ∧ ✷an → ✷b is strictly one-step complete. The axiomatisation of graded and probabilistic logics is more complicated, but still tractable in a sense recalled below. In the following, we fix a strictly one-step complete set R.

3 Generic Complexity Bounds

We proceed to develop a decision procedure for global consequence in coalgebraic hybrid logic, i.e., for Γ-satisfiability of formulas given a TBox Γ, where ABoxes are internalised using satisfaction operators. We translate the satisfiability problem into the problem of finding a winning strategy in a parity game. The latter will be played on a game board built from a Γ-closed set Σ of formulas.

Definition 3.1. Let Σ ⊆ F(Λ). A (Σ-)Hintikka set is a subset of Σ which is maximally consistent w.r.t. propositional reasoning. We say that Σ is closed if Σ is closed under subformulas, negation, and @t with t ∈ N(Σ), where we identify ¬¬φ with φ, @t¬φ with ¬@tφ, and @s@tφ with @tφ. We say that Σ is Γ-closed if Γ ⊆ Σ and Σ is closed. The Γ-closure of a set Δ is the smallest Γ-closed set containing Δ.

Let φ be a formula, to be checked for Γ-satisfiability. As φ is Γ-satisfiable iff @tφ is Γ-satisfiable for a fresh nominal t, we can assume that φ is an @-formula. We form the Γ-closure Σ of {φ} (which is of polynomial size in Γ, φ). Note that φ is Γ-satisfiable iff there exists a Γ-satisfiable @Σ-Hintikka set K such that φ ∈ K; as going through all such K yields an exponential factor and we are aiming for EXPTIME decidability, we can focus on deciding Γ-satisfiability of @Σ-Hintikka sets. We can then apply @-elimination [Myers et al., 2009]:

Definition 3.2. A hybrid formula is @-free if it does not contain occurrences of @. A set of @-formulas is @-eliminated if it consists of formulas @iρ with ρ @-free. For ρ ∈ Σ, ρ[K] denotes the @-free formula obtained by replacing every subformula @iχ of ρ not contained in further occurrences of @ by ⊤ if @iχ ∈ K, and by ⊥ otherwise.

One shows easily that a model satisfies K iff it satisfies the @-eliminated set {@iρ[K] | @iρ ∈ K}. Thus, we assume in the following w.l.o.g. that K is @-eliminated and hence that the Σ-Hintikka sets Ki = {ρ | @iρ ∈ K} (i ∈ N(Σ)) are @- free; intuitively, we have reduced to checking Γ-satisfiability of an ABox K. Note that the Ki need not be pairwise distinct. If one of the Ki does not contain Γ, then K is immediately rejected as Γ-unsatisfiable.

In the tableau system for global entailment, possible nontermination arises both from the presence of global assumptions, which may propagate indefinitely, as well as from the presence of nominals, which may force loops. The gametheoretic approach that we apply below allows us to deal with infinite paths in tableaux, and eliminates the need to consider blocking conditions. We introduce a notion of tableau graph that captures all possible tableaux, i.e., all possible rule applications at every node, within a single object:

Definition 3.3. If H is a Σ-Hintikka set, χ/ψ ∈ R, and σ is a substitution such that ψσ ∈ Prop(Σ) and H ⊢PL ¬ψσ, then ¬χσ is a demand of H. A Γ-tableau graph for K is a graph whose set of nodes consists of Σ-Hintikka sets and includes the Σ-Hintikka sets Ki, such that

1. for every demand ρ of a node H, there exists an edge H → G such that G ⊢PL ρ
2. whenever H ⊢PL i for some node H and some i ∈ N(Σ), then H =Ki,

3. H ⊇ Γ for every node H.

Theorem 3.4. The set K is Γ-satisfiable iff there exists a Γtableau graph for K.

Proof sketch. 'Only if' is by straightforward extraction of a tableau graph from a Γ-model for K. 'If' is by construction of a so-called coherent coalgebra structure ξ on the set of nodes in a tableau graph such that the graph becomes a supporting Kripke frame, i.e., for every node H, ξ(H) ∈ TY where Y is the set of successor nodes of H. Here, ξ is called coherent if for all ♥(ρ1, ..., ρn) ∈ Σ and all nodes H,

where ˆ ρ is the set of successor nodes G of H such that ρ ∈ G. Existence of a coherent structure ξ is proved by means of strict one-step completeness, analogously as in [Schr¨oder and Pattinson, 2009] but avoiding induction over the depth of nodes. Coherence then allows the inductive proof of a truth lemma, which entails that the model constructed satisfies both Γ and K.

As the nodes of the tableau graph are subsets of Σ, we obtain a small model property for hybrid coalgebraic logic relative to an arbitrary background theory.

Corollary 3.5. Every Γ-satisfiable formula φ is satisfiable in a Γ-model of exponential size in Γ and φ.

Having reduced the satisfiability problem to existence of tableau graphs, we now show that the latter can be further reduced to existence of winning strategies in certain parity games, as follows. The game is played by two players, Abelard (∀) and Eloise (∃); ∃ tries to prove that K is Γsatisfiable, while ∀ tries to prove the opposite. A move by ∀ consists in the choice of rule to be applied, giving rise to a demand, while a move by ∃ consists in the choice of a Hintikka set that satisfies the demand. Formally:

Definition 3.6 (Tableau Game). The Γ-tableau game for K is a graph game S = (B∃, B∀, E) where

• B∀, the set of positions owned by ∀, consists of an initial position init and all Σ-Hintikka sets H such that a) Γ ⊆ H and b) i ∈ N(Σ) =⇒ H = Ki.
• B∃, the set of positions owned by ∃, consists of pairs (R, σ), where R = χ/ψ is a rule in R and σ is a substitution such that ψσ ∈ Prop(Σ)
• E is the set of permissible moves, where ∀ may move from a Σ-Hintikka-set H to a pair (χ/ψ, σ) such that H ⊢PL ¬ψσ, and ∃ may move from (χ/ψ, σ) to a Σ-Hintikka set H such that H ⊢PL ¬χσ. Additionally, ∀ may move to any of the Ki from init.

The set of all positions on the game board is B = B∃ ∪ B∀. (Note that B∀ is a priori infinite if there are infinitely many rules; we will introduce additional assumptions later that allow reducing to a finite board.)

A full play in the tableau game is a finite or infinite sequence of moves (b0, b1, b2, . . . ) such that b0 = init, (bi, bi+1) ∈ E for all i ≥ 0, and - in case the sequence is finite - the last position has no permissible moves. A finite full play is lost by the player who owns the last position (and hence cannot move), and infinite full plays are won by ∃.

Remark 3.7. We note that the tableau game can be seen as a (very simple) parity game where we assign priority 0 to all positions of the game so that - by the parity condition - ∃ wins all infinite games [Mazala, 2001]. Hence, he tableau game is history free determined.

Definition 3.8. A history-free strategy for ∃ is a function f : B∃ → B such that (b, f(b)) ∈ E for all b ∈ B∃. We say that f is a winning strategy for ∃ if ∃ wins all full plays that conform with f in the obvious sense.

Lemma 3.9. Eloise has a history-free winning strategy in the Γ-tableau game for K iff there exists a Γ-tableau graph for K.

Proof sketch. 'If' is clear. 'Only if': construct the Γ-tableau graph starting from the initial set of nodes {Ki | i ∈ N(Σ)} and successively introducing additional nodes and edges according to the strategy of ∃ for every possible move of ∀, i.e., for all arising demands.

We now show that the existence of a winning strategy for ∃ in the tableau game can be decided in exponential time, subject to a mild condition on the rule sets that is satisfied in all our examples. We require the modal tableau rules to be tractable in a similar sense as in Schr¨oder and Pattinson [2009]; the main condition here is that one may restrict to rule sets with at most polynomial-size codes (regarding the remaining conditions, we can be slightly more generous in the context of EXPTIME bounds relevant here).

Definition 3.10. The set R of modal rules is EXPTIMEtractable if there exists a coding of the rules such that, up to propositional equivalence, all demands of a Hintikka set can be generated by rules with codes of polynomially bounded size, and such that validity of codes, matching of rule codes for χ/ψ ∈ R to Hintikka sets H (in the sense of finding σ such that H ⊢PL ¬ψσ), and membership of clauses in a CNF of a rule premise are all decidable in EXPTIME.

Lemma 3.11. If R is EXPTIME-tractable, then it can be decided in EXPTIME whether ∃ has a winning strategy in the Γ-tableau game for K.

Proof Sketch. Given that the rule set is tractable, we may replace the positions B∃ owned by ∃ by codes of polynomial size in Γ,K. This leads to a game board whose size n is at most exponential in Γ,K. As we have a parity game with only one priority, it takes at most O(n4 ) ∗ k steps to determine whether ∃ has a winning strategy [Klauck, 2001], where k is such that one can decide in at most k steps whether (b, b′ ) ∈ E. Tractability of the rule set guarantees that k is at most exponential, so that we obtain overall complexity EXPTIME .

Corollary 3.12. If R is EXPTIME-tractable, then Γsatisfiability of formulas φ over general TBoxes Γ is decidable in EXPTIME.

The above corollary yields decidability in EXPTIME of reasoning over general TBoxes for all logics mentioned in Example 2.2. In particular, this reproves the known tight upper bound for hybrid K (which follows from an EXPTIME upper bound for the graded μ-calculus [Areces and ten Cate,

2007]), as well as for the description logics ALCOQ and, with minor adjustments of the argument, ALCHOQ [Tobies, 2000], and in fact even the more expressive ALCHOQ@ that features satisfaction operators [Liu et al., 2006]. The use of games in this context appears to be new. The (tight) upper bounds for TBox reasoning in probabilistic hybrid logic, conditional hybrid logic, and hybrid coalition logic are, to our knowledge, previously unknown. We discuss some examples of this type in more detail below.

4 Two Views on Probabilistic Successors

We discuss two applications that highlight the generality of our results. In both examples, we combine classical relational successors and uncertainty, but in two different ways. Both are phrased in terms of descendancy, where states in a model represent persons.

4.1 Probabilistic Successors

We imagine a situation where we only have probabilistic knowledge about the offspring of a certain person. Suppose for instance that the probability that c (Catherine Carey) is a child of h (Henry VIII) is known to be at least 0.8, and similarly we know that h′ (Henry Carey) is a child of h with likelihood 0.6. To model this situation, we consider a structure of type C → DP(C) where P(X) is the powerset of a set X and D(X) = {μ : X → [0, 1] | supp(μ) is finite, ∑x∈X μ(x) = 1} is the set of finitely supported probability distributions over X as in Example 2.2. In other words, given a person x ∈ C, an application of the structure map yields a probability distribution over sets (!) of persons. If this distribution assigns probability p to a set C′ ⊆ C, we interpret this as the fact that the probability that C′ are (precisely) the children of x equals p. (Note that this model applies primarily when x is male.)

This situation can be syntactically described using modal operators of the form Lp✸, where Lp✸φ reads 'the probability that there exists a successor that satisfies φ is at least p', together with the companion modality Lp✷ expressing the same statement relative to all successors.

Assume we know that the probability that every king has at least one illegitimate child is at least 0.8. This is expressed using the global assumption

while the above assertions about Catherine and Henry Carey take the form

Moreover, we know that Henry is a king, and m (Mary) is certainly a child of Henry, and either c or h′ is illegitimate, whereas e is legitimate, which we express by

Now consider the concept

asserting that all children of a king are legitimate with probability at least 0.9. This concept is satisfiable, but h is not an instance of c2 (as e is a legitimate child of h).

Similarly, the ABox

formalising that c is legitimate and c and h′ are the only possible illegitimate children of h is satisfiable (and the global assumption forces that h′ be a child of h with likelihood at least 0.8) but it becomes unsatisfiable if we stipulate for example that h′ is a child of h with probability at most 0.7. The proof rules that govern this situation are a straightforward combination of the rules discussed in [Schr¨oder and Pattinson, 2009], which immediately yields tractability of the ensuing combined rule set. As a consequence, we have that global consequence for the logic of probabilistic successors is decidable in EXPTIME.

4.2 Probabilistic Identities

Now let us suppose that someone internal to Henry's court has observed that none of the children of c′ (Catherine of Aragon) had really died, but they were rather removed from court, and we are left with only probabilistic knowledge concerning their identities.

To model this situation, we need to consider a different combination of relational successors and probability distributions. Our knowledge base is modelled by structures of the form C → P(D(C)) where P and D are as above. The main difference is now that, from each state of the model, we can observe a set of relational successors (corresponding to the person's offspring), but each successor carries a probability distribution over the model that expresses uncertainty concerning the successor's identity.

Syntactically, this leads to modal operators of the form ✸Lp asserting that there exists a (relational) successor that satisfies a given formula with probability at least p. However, we use a slightly richer set of modal operators, where we can interpose propositional connectives between the relational and probabilistic operators. Formally, this leads to a two-sorted logical language where one sort describes relational successors and the second models quantitative uncertainty; tractability of such combinations is established in [Schr¨oder and Pattinson, 2007], so that we obtain decidability in EXPTIME of global consequence in this situation (formally, the logic of the previous section arises as a similar combination, the second sort corresponding to possible worlds).

Suppose that c′ had one female child, whose identity is known to be m (Queen Mary) with certainty, and she also had a male child, believed to be a with likelihood at least 0.2 and b with likelihood at least 0.8. We take it for granted that a queen's offspring is always legitimate, leading to the global assumption

where we have made use of the ability to apply propositional connectives to subformulas of the same (here: probabilistic) type. This assumption expresses that at least one of the possible candidates (with non-zero probability) for any given child of a queen, namely the actual child, must be legitimate.

In addition, we have the ABox

that formalises our assumptions concerning c′ 's offspring. We may now ask whether it is possible that both a and b are illegitimate, i.e.,

@aillegitimate ∧ @billegitimate.

This formula is not satisfiable as it would violate the global assumption. In contrast, the statement that a queen has at least one child who will be queen with likelihood at least 0.7, i.e., the formula

is consistent with our (hypothetical) knowledge - we may, e.g., consider models satisfying @mqueen.

5 Conclusion

We have extended the algorithmic framework surrounding coalgebraic hybrid logic [Myers et al., 2009] to deal with global logical consequence. In description logic terms, we internalise the ABox and provide support for concept satisfiability and instance checking relative to a general TBox. Specifically, we have established a small model property for coalgebraic hybrid logic over general TBoxes (Corollary 3.5), and a criterion for EXPTIME decidability of global consequence (Corollary 3.12). The prime achievement of this work is its generality: instantiations of the coalgebraic framework yield new EXPTIME bounds for a large number of modal and description logics far beyond Kripke semantics including various conditional logics, coalition logic, and logics for uncertainty. The complexity bounds are obtained by reducing satisfiability to the existence of winning strategies on a game played on a tableau graph, which also implies completeness of a tableau calculus with suitable blocking conditions. Further extensions of the framework, such as local binding [Horrocks et al., 2007] and the addition of temporal operators via suitable fixpoints, as well as the analysis of further reasoning tasks and the possibility of efficient reasoning using SMT solvers for local tasks, are the subject of ongoing research.