I will begin by explaining an optimal tableau-based algorithm for checking ALC-satisfiability which uses “global caching” and which appears to work well in practice. The algorithm settles a conjecture that “global caching can lead to optimality”. I will then explain how “global caching” can be extended to “global state caching” for inverse roles, thereby extending the result to ALCI-satisfiability, and converse roles in general. Finally, I will explain how “global caching” can be used to give optimal “on the fly” tableau decision procedures for some fixpoint logics. Finally, some open questions. The talk is intended to be expository so it will be at a fairly high level.
This overview is based on joint work with Linh Anh Nguyen [
The tableau method is a very general method for automated reasoning and
has been widely applied for modal logics [
For fixpoint logics like PLTL, CTL and PDL, optimal tableau methods are
possible if we proceed in stages with the first stage building a cyclic graph,
and subsequent stages pruning nodes from the graph until no further pruning is
possible or until the root node is pruned [
Thus a long-standing open problem in tableau methods for modal, description, and fixpoint logics has been to find an optimal and “on the fly” method for checking satisfiability which only requires exponential time when it is really necessary. We describe such tableau methods for each of the logics ALC, ALCI, and PDL, but before doing so, we clarify some terminology and ask the expert reader to bear with us. In particular, we leave the actual search strategy unspecified even though depth-first search is often used in practice.
A tableau is a tree of nodes where the children of a node are created by applying a tableau rule to the parent and where each node contains a finite set of formulae. We refer to these formulae as the “contents” of a node, noting that the term “label” is also used to mean the same thing. Thus a label is not a name for a Kripke world as in some formulations of “labelled tableaux”. The ancestors of a node are simply the nodes on the unique path from the root to that node.
A leaf node is “closed” when it can be deemed to be unsatisfiable, usually because it contains an obvious contradiction like p and ¬p. A leaf is “open” when it can be deemed to be satisfiable, usually when no rule is applicable to it, but also when further rule applications are guaranteed to give an infinite branch. A branch is closed/open if its leaf is closed/open. The aim of course is to use these classifications to determine whether the root node is satisfiable or unsatisfiable. But the tableau used in modal logics and those used in description logics are dual in a sense which is explained next.
Traditional Beth Tableaux are Or-trees. Traditional modal tableaux a la` Beth [
For most (non fix-point) modal and description logics, ancestor cycles are
“good” in that a branch ending with a node blocked by an ancestor can be
soundly deemed to be satisfiable. In modal tableau, such a branch will cause
backtracking to a higher node where a different and-choice can be made in the
hope of finding a choice that closes its branch. In description logic tableau, such a
branch will cause no backtracking. In description logic tableaux, where branches
are all and-branches, a further refinement called “anywhere blocking” [
Global Caching. Now consider the following notion of “global caching” where each tableau node contains (is labelled with) a unique set of formulae: Global caching: each tableau node is processed at most once in the search space. Our notion of global caching is an immediate foundation for an exptime procedure if the search space contains at most an exponential number of different nodes and as long as the “processing” at each node requires at most exponential time, both with respect to the size of the given problem. Moreover, it can replace all of the previously mentioned notions of equality-blocking and caching simultaneously because it does not rely on knowing the satisfiability or unsatisfiability status of the cached nodes viz: Ancestor equality blocking occurs if the ancestor (with unknown status) is the first occurrence of the repeating node in the whole search space, otherwise, even the ancestor would not have been re-created but would have been replaced by a cache-hit to its first occurrence (with status unknown); Anywhere equality blocking occurs without the extra conditions required by the existing methods for the same reasons; Caching occurs automatically since a previously seen node whose status is known as unsatisfiable or satisfiable must have been processed, so it will never be processed again. wwooooodoonoeooooooo rt Given a TBox T and a concept/formula D, both in negation normal form, our method searches for an model which satisfies D w.r.t. T by building an and-or graph G with root node τ containing T ∪ {D}.
A node in the constructed and-or graph is a record with three attributes: content: the set of concepts/formulae carried by the node status: {unexpanded, expanded, sat, unsat} kind: {and-node, or-node, leaf-node}
The root node has initial status unexpanded and our method constructs the and-or graph using a traditional strategy explained shortly. But we interleave this generation strategy with a propagation phase which propagates the status of a node throughout the graph. We explain each in turn.
Our strategy for building the and-or graph applies the rules for
decomposing ⊓ and ⊔ repeatedly until they are no longer applicable to give a “saturated”
node x, and then applies the ∃-rule which creates a child node for x
containing T ∪ {C} ∪ {D | ∀r.D ∈ x} for each ∃r.C ∈ x. The addition of the TBox T
to such a child is a naive way to handle TBoxes but suffices for our needs. We
now saturate any such child to obtain a saturated node y, then apply the ∃-rule
to y, and so on, until we find a contradiction, or find a repeated node, or find a
saturated node which contains no ∃-formulae. For uniformity with our method
for the extensions to inverse roles and PDL, we explore/expand children in a
left to right depth-first manner, although any search strategy can be used for
ALC [
An application of ⊔ to a node v causes v to be an or-node, while an application of ⊓ or (∃R) to a node v causes v to be an and-node. Notice that our method uses the (∨) and (∃) rules which use both or-branching and and-branching as summarised in Section 1. The crucial difference from traditional tableau methods is that we create the required child in the graph G only if it does not yet exist in the graph: this step therefore uses global caching. Notice that the required child need not be an ancestor but can exist on any previous branch of the tableau. For example, as shown in Figure 1, suppose the current node is x and that the rule applied to x generates a node y′ which duplicates y. The node y′ is not put into G, but y becomes the child of x instead. Thus, G is really a rooted and-or tree with cross-branch edges to nodes on previously created branches like that from x to y or from v to u, or edges to ancestors like that from w to z. The problem of course is to show that this remains sound.
The propagation phase begins whenever we determine the status of a node as either unsat or sat as explained next.
A generated node that contains both A and ¬A for some atomic formula A becomes a leaf-node with status unsat (i.e. unsatisfiable w.r.t. T ). A generated node to which no tableau rule is applicable becomes a leaf-node with status sat (i.e. satisfiable w.r.t. T ). Both conclusions are irrevocable because each relies only on classical propositional principles and not on modal principles. We therefore propagate this information to the parent node v using the kind (or-node/and-node) of v and the status of the children of v, treating unsat as irrevocably false and sat as irrevocably true. That is, an or-node gets status sat as soon as one of its children gets status sat, and gets status unsat when all of its children get status unsat. Dually for and-nodes. In particular, it does not matter whether the parent-child edge is a cross-branch edge or whether it is a traditional top-down edge. If these steps cannot determine the status as sat or unsat, then the rule application sets the status to expanded and we return to the generation phase.
The main loop ends when the status of the initial node τ becomes sat or unsat, or when no node has status unexpanded. In the last case, all nodes with status 6= unsat are given status sat (effectively giving the status “open” to tableau branches which loop to an ancestor) and this status is propagated through the graph to obtain the status of the root node as either unsat or sat.
This algorithms thus uses both caching and propagation techniques and runs
in exptime [
Recall that the standard strategy for rule applications in tableau algorithms is to apply the rules for decomposing ⊓ and ⊔ repeatedly until they are no longer applicable, giving a “saturated” node which contains only atoms, negated atoms, ∀-formulae and ∃-formulae. Let us call such a “saturated” node a state and call the other nodes prestates. Thus the only rule applicable to a state x is the ∃-rule which creates a node containing T ∪ {C} ∪ {D | ∀r.D ∈ x} for each ∃r.C ∈ x. The standard strategy will now saturate any such child to obtain a state y, then apply the ∃-rule to y, and so on, until we find a contradiction, or find a repeated node, or find a state which contains no ∃-formulae. Let us call x the parent state of y since all intervening nodes are not states. (a) x ps0 psk
∃r.C z toosmall ({E | ∀r`.E ∈ z} \ x) ∈ altx
∃r.C (b) x ps0 psk z y (c) x
∃r.C ps0 psk z EVEVEEVEVEV""VVVVVVVVVVVV++ yn+/zn y y1+/z1 · · ·
When inverse roles are present, we require that {E | ∀r`.E ∈ y} ⊆ x, since y is then compatible with being an r-successor of x in the putative model under construction. If some ∀r`.E ∈ y has E ∈/ x then x is “too small”, and must be enlarged into an alternative node x+ by adding all such E. If any such E is a complex formula then the alternative node x+ is not “saturated”, and hence not a state. So we must saturate it using the ⊓/⊔-rules until we reach a state. That is, a state x may conceptually be “replaced” by an alternative prestate x+ which is an enlargement of x, and which may have to be saturated further in order to reach a state.
Our algorithm handles these “alternatives” by introducing a new type of node called a special node, introducing a new type of status called toosmall, allowing states to contain a field alt for storing these alternatives, and ensuring that a state always has a special node as its parent. When we need to replace a state x by its alternatives, the special node above x extracts these alternatives from the altx field and creates the required alternative nodes as explained next.
Referring to Fig. 2, suppose state x has an r-successor prestate ps0, and further saturation of ps0 leads to prestate psk, and an application of an ⊓/⊔-rule to pk will give a state y. Instead of directly creating y, we create a special node z which carries the same set of formulae as would y, and make z a child of psk. We now check whether z is compatible with its parent state x by checking whether {E | ∀r`.E ∈ z} ⊆ x. If z is not compatible then we mark z as toosmall, and add {E | ∀r`.E ∈ z} \ x to the set of alternative sets contained in altx, without creating y, as shown in Fig. 2(a). If z is compatible with x, we create a state y if it does not already exist, and make the new/old y a child of z, as in Fig. 2(b).
Suppose that y is compatible with x and that either y is already toosmall or becomes so later because of some descendant state w of y. In either case, the attribute alty then contains a number of sets y1, y2, . . . , yn (say), and the toosmall status of y is propagated to the special node z. In response, z will create the alternatives y1+, y2+, . . . , yn+ for y with yi+ := y ∪ yi. If yi+ is a state then our algorithm will create a special node zi below z, and if zi is compatible with x then y+ will be created or retrieved and will become the child of zi as in (b) else iyi+ will not be created and zi will be marked as toosmall as in (a). If yi+ is not a state then it will be created as a direct prestate child of z. Figure 2(c) captures this by using yi+/zi to stand for either yi+ or zi. Each of these new non-special nodes will eventually be expanded by our algorithm but now the “lapsed” special node z will be treated as a ⊔-node.
Global State Caching. The complexities introduced by alternative nodes makes it difficult to use global caching so instead we use “global state caching”: that is, the saturation phase is allowed to re-create prestates that occur on previous branches, but states cannot be duplicated so we must use cross-branch edges to their previous incarnations.
The resulting algorithm runs in exptime [
Our algorithm starts at a root containing a given formula φ and builds an andor tree in a depth-first and left to right manner to try to build a model for φ. The rules are based on the semantics of PDL and either add formulae to the current world using Smullyan’s α/β rules from Table 1, or create a new world in the underlying model and add the appropriate formulae to it. For a node x, the attribute Γx carries this set of formulae.
The strategy for rule applications is the usual one where we “saturate” a node using the α/β-rules until they are no longer applicable, giving a “state” node s, and then, for each haiξ in s, we create an a-successor node containing {ξ} ∪ Δ, where Δ = {ψ | [a]ψ ∈ s}. These successors are saturated to produce new states using the α/β-rules, and we create the successors of these new states, and so on.
Our strategy can produce infinite branches as the same node can be created
repeatedly on the same branch. We therefore “block” a node from being created
if this node exists already on any previous branch, thereby using global caching
again, but now nodes are required to contain “focused sets of formulae” [
Our tableau must “fulfil” every formula of the form hδiϕ in a node but only eventualities, defined as those where δ contains ∗-connectives, cause problems. If hδiϕ is not an eventuality, the α/β-rules reduce the size of the principal formula, ensuring fulfilment. If hδiϕ is an eventuality, the main problem is the wwooooodoonoeooooooo rt β-rule for formulae of the form hγ∗iϕ. Its left child reduces hγ∗iϕ to a strict subformula ϕ, but the right child “reduces” it to hγihγ∗iϕ. If the left child is always inconsistent, this rule can “procrastinate” an eventuality hγ∗iϕ indefinitely and never find a world which makes ϕ true. This non-local property must be checked globally by tracking eventualities.
Consider Fig. 3, and suppose the current node x contains an eventuality ex. We distinguish three cases. The first is that some path from x fulfils ex in the existing tree. Else, the second case is that some path from x always procrastinates the fulfilment of ex and hits a forward-ancestor of x on the current branch: e.g. the path x, y, v, u, w, z. The forward-ancestor z contains some “reduction” ez of ex. The path from the root to the current node x contains the only currently existing nodes which may need further expansion, and may allow z to fulfil ez at a later stage, and hence fulfil ex. We call the pair (z, ez) a “potential rescuer” of ex in Γx. The only remaining case is that ex ∈ Γx is unfulfilled, has no potential rescuers, and hence can never become fulfilled later, so x can be “closed”. The machinery to distinguish these three cases and compute, if needed, all currently existing potential rescuers of every eventuality in Γx is described next.
A tableau node x also contains a status stsx. The value of stsx is the constant closed if the node x is closed. Otherwise, the node is “open” and stsx contains a α ϕ ∧ ψ [γ ∪ δ]ϕ [γ∗]ϕ hψ?iϕ hγ; δiϕ [γ; δ]ϕ α1 ϕ [γ]ϕ ϕ ϕ hγihδiϕ [γ][δ]ϕ α2 ψ [δ]ϕ [γ][γ∗]ϕ ψ β ϕ ∨ ψ hγ ∪ δiϕ hγ∗iϕ [ψ?]ϕ β1 ϕ hγiϕ ϕ ϕ β2 ψ hδiϕ hγihγ∗iϕ ∼ ψ function prs which maps each eventuality ex ∈ Γx to ⊥ or to a set of pairs (v, e) where v is a forward-ancestor of x and e is an eventuality. The status of a node is determined from those of its children once they have all been processed. A closed child’s status is propagated as usual, but the propagation of the function prs from open children is more complicated. The intuition is that we must preserve the following invariant for each eventuality ex ∈ Γx: if ex is fulfilled in the tree to the left of the path from the root to the node x then prsx(ex) := ⊥, else prsx(ex) is exactly the set of all potential rescuers of ex in the current tableau.
An eventuality ex ∈ Γx whose prsx(ex) becomes the empty set can never become fulfilled later, so stsx := closed, thus covering the three cases as desired.
Whenever a node n gets a status closed, we interrupt the depth-first and leftto-right traversal and invoke a separate procedure which explicitly propagates this status transitively throughout the and-or graph rooted at n. For example, if z gets closed then so will its backward-parent w, which may also close u and so on. This propagation (update) may break the invariant for some eventuality e in this subgraph by interrupting the path from e to a node that fulfils e or to a potential rescuer of e. We must therefore ensure that the propagation (update) procedure re-establishes the invariant in these cases by changing the appropriate prs entries. At the end of the propagation (update) procedure, we resume the usual depth-first and left-to-right traversal of the tree by returning the status of n to its forward-parent. This “on-the-fly” nature guarantees that unfulfilled eventualities are detected as early as possible.
Our algorithm terminates, runs in exptime, and formula φ is satisfiable iff
the root is open [
We have shown that global caching can indeed be formalised in the description
of tableaux algorithms in a sound manner to give an exptime algorithm for
checking satisfiability w.r.t. a TBox in ALC [