The tableau algorithm is one of the main reasoning algorithms employed by DL reasoners. It is also often taught as a reasoning technique at DL courses at universities. As the algorithm proves the existence of a model for a knowledge base by constructing a completion tree, the best way to understand this mechanism is to construct this tree graphically. Realization of this process on the blackboard is usually very laborious, and mainly the backtracking is chaotic. We have developed SIVA { a simulation tool for ALC, visualizing the whole process from initializing a vocabulary and a knowledge base, to building a completion tree step by step by application of the tableau rules. It allows easy backtracking to any of the previous states. SIVA is freely available as an online application.
A signi cant amount of research in DL is focused on tableau reasoning algorithms
[25,15,13,14,12,10,11, i.a.]. They are also taught to students during courses on
knowledge representation and reasoning. Visualization of the tableau algorithm
on the blackboard is helpful, but it is usually quite messy, especially in cases
when the algorithm needs to backtrack. Indeed, a body of research in algorithms
education has been devoted to development of tools for algorithm visualization
[
There is a number of tools [22,28,7,23,24,4,31,18,17,3,6, i.a.] for ontology
visualization. Though as noted by a recent survey [
If we extend our outlook beyond ontologies and description logics, both
LoTREC [
To our best knowledge, none of these tools allows full step-by-step control of
the user while working with the visualized proof, where user has to gure out
the next step of the proof. This is possible e.g. in the Tableau Editor [
We have developed and implemented a web application enabling step-by-step
simulation of the tableau algorithm for the DL ALC [
We believe such a tool is a useful aid for students learning the tableau algorithm. In the future, we plan to extend the application to enable reasoning over more expressive DLs, and to enable the user to add custom tableau rules or blocking methods. We consider the latter two upgrades to be useful also for researchers in their works. 2
We build on top of the ALC DL [
A knowledge base K = (T ; A) consists of a TBox T and an ABox A. A TBox is a nite set of GCI axioms of the form C v D, where C; D are concepts. An ABox is a nite set of concept assertions of the form C(a), and role assertions of the form R(a; b), where a; b 2 NI, C is a concept, and R 2 NR.
An interpretation is a pair I = ( I ; I ), where I 6= ; is a domain, and the interpretation function I maps each individual a 2 NI to aI 2 I , each atomic concept A 2 NC to AI I , each role R 2 NR to RI I I in such a way that the constraints in Table 1 are satis ed.
Two concepts C and C0 are equivalent if CI = C0I for every interpretation I. An interpretation I satis es an axiom ' (denoted I j= ') if the respective constraint in Table 1 is satis ed. It is a model of a knowledge base K if it satis es all axioms included in K.
De nition 1 (Model). An interpretation I is a model of a knowledge base K = (T ; A) (denoted I j= K) i I j= ' for all ' 2 T [ A.
The main DL decision problems deal with concept satis ability checking, axiom entailment checking, and consistency checking of a knowledge base.
A concept is satis able w.r.t. a knowledge base if there is a model of this knowledge base interpreting the concept into a non-empty set.
De nition 2 (Satis ability). A concept C is satis able w.r.t. a knowledge base K i there is a model I of K s.t. CI 6= fg.
An axiom is entailed by a knowledge base if it is satis ed by all the models of this knowledge base.
De nition 3 (Entailment). A knowledge base K entails an axiom ' (denoted K j= ') i I j= ' for each model I of K.
A knowledge base is consistent, if there is at least one interpretation I such that I j= K, i.e. it has at least one model.
De nition 4 (Consistency). A knowledge base K is consistent, if there is at least one interpretation I that is a model of K.
In fact, it is well known that all the decision problems stated above are
reducible to the consistency checking problem [
Lemma 1 (Satis ability reduction). Given a DL knowledge base K, a concept C is satis able w.r.t. K i K [ fC(a)g is consistent for some new individual a.
Lemma 2 (Subsumption entailment reduction). Given a DL knowledge base K, and concepts C and D, K j= C t D i K [ fC u D(a)g is consistent for some new individual a.
Lemma 3 (Assertion entailment reduction). Given a DL knowledge base K, a concept C, and an individual a, K j= C(a) i K [ f:C(a)g is inconsistent.
A concept C is in negation normal form (NNF) if the complement
constructor : stands only in front of atomic concepts in C. From now on, by nnf(C) we
denote a concept C0 in NNF that is equivalent to C. At least one such concept
always exists [
Thanks to reductions, it is su cient to have an algorithm that solves the consistency checking problem, and so each of the listed decision problems can be solved via reduction. Perhaps the most common reasoning technique in DL is the tableau algorithm.
This algorithm works by proving the existence of a model of K by constructing it. More precisely, it works on a structure called completion tree that is iteratively extended by applying a set of tableau rules until it corresponds to a model, or until it is clear that this is not possible.
De nition 5 (Completion tree). A completion tree (CTree) is a triple T = (V; E; L) where (V; E) is an oriented graph with a set of nodes V and a set of edges E, and L is a labeling function that assigns a label to all nodes and edges of T as follows: { L(v) is a set of concepts in NNF for a node v 2 V , { L(hx; yi) is a set of roles for an edge hx; yi 2 E.
We say that a node y 2 V is a successor of a node x 2 V in a CTree T = (V; E; L) if hx; yi 2 E, and that a node y 2 V is a descendant of x 2 V if there is a path from x to y. A node y is an R-successor if y is a successor of x and R 2 L(hx; yi).
To nd out whether a knowledge base K is consistent, the algorithm tries to construct a corresponding CTree, that is free of any local inconsistency, which is called a clash; i.e., it tries to assure that the CTree is clash-free. De nition 6 (Clash). There is a clash in L(v) for a node v 2 V of a CTree T = (V; E; L), if fC; :Cg 2 L(v) for some concept C. A CTree is clash-free if none of its nodes contains a clash.
However, some models may be in nite [
De nition 7 (Blocked node). Given a CTree T = (V; E; L), a node y 2 V is blocked if it is a descendant of another node x 2 V s.t.: { either L(y) L(x); { or x is blocked.
Finally, the algorithm is presented in De nition 8. For K = (T ; A) it rstly initializes the CTree T by encoding into it the explicit statements from the ABox A. After this initialization, tableau expansion rules are repetitively applied in order to expand a CTree. If a clash-free and complete CTree is found, the algorithm answers that K is consistent, otherwise that K is inconsistent. De nition 8 (Tableau algorithm for consistency checking). Input: K = (T ; A) in NNF Output: answers if K is consistent or not Steps: 1. Initialize a CTree T as follows: (a) V := fa j individual a occurs in Ag; (b) E := fha; bi j R(a; b) 2 A for some role Rg; (c) L(a) := fnnf(C) j C(a) 2 Ag for all a 2 V ; (d) L(ha; bi) := fR j R(a; b) 2 Ag for all a; b 2 V ; 2. Apply tableau expansion rules from De nition 8 while at least one is applicable: u-rule: t-rule: T -rule: if C u D 2 L(x), x 2 V is not blocked, and
fC; Dg * L(x) then L(x) L(x) [ fC; Dg if C t D 2 L(x), x 2 V is not blocked, and
fC; Dg \ L(x) = ; then either L(x) L(x) [ fCg or
L(x) L(x) [ fDg if 8R:C 2 L(x), x 2 V is not blocked, and y is R-successor of x and
C 2= L(y) then L(y) L(x) [ fCg if 9R:C 2 L(x), x 2 V is not blocked, and
there is no R-successor y of x s.t. C 2 L(y) then create a new anonymous node z and
V V [ fzg and
L(z) = fCg if C v D 2 T , x 2 V is not blocked, and
nnf(:C t D) 2= L(x) then L(x) L(x) [ fnnf(:C t D)g 3. Answer \K is consistent" if T is clash-free, otherwise answer \K is inconsistent".
The process of building a CTree is nondeterministic. Speci cally, there are two kinds of rules. All rules but the t-rule are AND-rules : they are deterministic rules with a single possible way of application. The t-rule is an OR-rule: a nondeterministic rules with multiple possible ways of application (two, in this case).
In order to explicitly represent the nondeterministic choices and backtracking
done by the algorithm, we track them in a structure called a tableau.1
1 We are aware that this notion of tableau is di erent from how this term is usually
used in DL literature [
(hx; yi) = (r; u; C) if an OR-rule r was applied on a node u from (x) yielding (y) in which L(u) was extended by C; in this case x has as many successors as many are possible nondeterministic choices for r on u.
The root node in is the only node without incoming edges and represents the initial state of the reasoning process. 4
Within our work, we have proposed and implemented a general purpose algorithm visualization system called SIVA (System of Interactive Visualizations of Algorithms). While designing SIVA, a considerable amount of attention has been paid to its extensibility and modularity. Currently, the most signi cant contribution of our work to the eld of DL is enabling visualization and control over every step of the completion tree version of the tableau algorithm reasoning process in ALC, which is provided by SIVA's modules we have implemented (DL module and its submodule CTreeTableauReasoning). SIVA's extensibility promotes its future development, due to which support for other description languages or visualization of di erent algorithms could be implemented.
Our implementation of the tableau algorithm for ALC, utilizes an abstract tableau, which is not constrained to be used with any particular logic formalism. The tableau is stored as a tree-like data structure with exactly one of its nodes representing the initial and one node representing the current state of the reasoning process. Every tableau node except the initial one contains an exact description of reversible actions that transform the state represented by their parents to the state represented by them, which makes them freely traversable. In case of the completion tree version of the tableau algorithm for DL, each node of the tableau describes how an application of a tableau rule a ects the completion tree.
The CTreeTableauReasoning module enables access to the completion tree data structure and its interactive visualization. The completion tree is represented by a graph-like data structure, whose nodes and edges are labeled by sets of concepts and roles, respectively. While applying tableau expansion rules, the application automatically extends respective labels of nodes and edges and transforms concepts to their NNF.
The DL module processes input in the form of DL expressions in original mathematical notation and provides a virtual keyboard with all necessary mathematical symbols. User input is automatically parsed and checked for errors, which have to be xed before choosing a desired DL problem to solve. SIVA currently supports three types of problems within ALC, which can be interactively solved using the completion tree version of tableau algorithm: { concept satis ability checking, { instance checking, { knowledge base consistency checking.
All instances of these decision problems are solved by reducing them to knowledge base consistency checking. SIVA's extensible design allows broadening its support beyond ALC and the mentioned set of reasoning problems in DL.
Functionality of external modules can be made accessible to users through SIVA's API by providing a so called workspace { a container component, which assembles all visual and functional components required to perform actions speci ed by the module. Our implementation of CTreeTableauReasoning contains a workspace that assembles visualizations and functionality of DL vocabularies, knowledge bases, completion trees and tableaux and enables communication between these components.
We have implemented SIVA as a heavily client-side oriented web application. It has been built using the React framework with TypeScript as the main scripting language. The application's internal work ow follows the Flux architecture, which is standardly used within React-based applications. 5
During the initial access of SIVA, the user is provided by a list of workspaces available for initialization, which currently contains only the workspace allowing visual simulation of reasoning using the completion tree version of tableau algorithm in ALC. Prior to any actual reasoning, the user has to establish a DL vocabulary and a knowledge base, either by typing them manually into designated input boxes or by loading existing ones, which have been previously exported using our application.
In Fig. 1 an example knowledge base about owners of potentially murder weapons (PMW) and a butcher owning a meat cleaver is shown. If the provided input is error-free, the user can choose one of the supported types of reasoning problems to solve and de ne its instance using the provided input controls.
While solving a reasoning problem, the application guides the user through the completion tree (Fig. 4) initialization phase, which, due to reduction to knowledge base consistency checking, always consists of creating nodes representing individuals from a non-empty ABox.
Afterwards, the user can freely apply tableau rules, essentially replacing the algorithm's non-determinism. Application of the T -rule is accessed through a dedicated button present in the labels of completion tree nodes and it is performed by choosing a TBox axiom associated with the desired T -rule (Fig. 2). All other tableau rules are applied by simply clicking on concepts in labels of nodes associated with the tableau rule. When applying the t-rule, the user also chooses one of the two ways he wants it to be applied (Fig. 3).
After encountering a clash or a fully expanded completion tree, the application visually informs the user and no more tableau expansion rules can be applied. The user can utilize the tableau (Fig. 5) in order to backtrack the reasoning state to any of the previously discovered ones. The tableau is visualized as a simple rooted tree, whose nodes can be freely traversed by clicking on them, which transforms the current state to the one represented by the clicked tableau node. The user can also quickly traverse the states represented by the current tableau node's parent and its children by using dedicated buttons without the need to access the tableau visualization.
Our application is accessible online at http://siva.6f.sk/. 6
We have developed SIVA { an educational tool for visual simulation of the tableau algorithm for the description logic ALC. The web application is freely accessible. It allows the user to create a knowledge base, and to solve a decision problem by running a step-by-step simulation of the tableau algorithm. Available decision problems are consistency checking, instance checking, and concept satis ability.
In the future, we would like to extend the application for more expressive
description logics, and to allow the user to specify own tableau rules,
blocking strategy, etc. We hope that this could make our tool interesting also for
researchers. The application can also be extended by some standard tableau
expansion strategies or optimization techniques. We would like to integrate the
application with a course ware, such as Moodle [