We present an ongoing implementation of a KE-tableau based reasoner for a decidable fragment of strati ed elementary set theory i(D) (shortly DL4D; ). The reexapsroensseirncghtehckesdtehsecrcipotnisoinstelongciyc oDf LDhL4L4DQ;S-kRn;owledge bases (KBs) represented in set-theoretic terms. It is implemented in C++ and supports DL4D; -KBs serialized in the OWL/XML format. To the best of our knowledge, this is the rst attempt to implement a reasoner for the consistency checking of a description logic that is represented via a fragment of set theory that can also classify standard OWL ontologies.
Computable set theory is a research eld rich of decidability results, however
only recently some of its fragments have been applied in the context of knowledge
representation and reasoning for the semantic web. Such e orts are motivated
by the characteristics of the considered set-theoretic fragments. These provide
very expressive and unique formalisms that combine the modelling capabilities
of a rule language with the constructs of description logics. In particular, the
set-theoretic fragment 4LQSR [
In [
The description logic DL4D; admits full negation, union and intersection of
concepts and abstract roles, concept domain and range, and existential and
minimum cardinality restriction on the left-hand side of inclusion axioms. It also
? Work supported by Gruppo Nazionale per il Calcolo Scienti co (GNCS-INdAM).
supports role chains on the left-hand side of inclusion axioms and properties on
roles such as transitivity, symmetry, re exivity, and irre exivity. Thanks to its
4; can represent expressive ontologies, such as, for instance,
expressiveness, DLD
OntoCeramic [
Since existential quanti cation is admitted only on the left-hand side of
in4; is less expressive than logics such as SROIQ(D) [
4; is a powerful rule language able to express rules with negated In addition, DLD atoms such as P erson(?p) ^ :hasHome(?p; ?h) =) HomelessP erson(?p). Notice that rules with negated atoms are not supported by the Semantic Web Rule Language (SWRL).
By resorting to the algorithm introduced in [
Our reasoner, still in beta-testing, is available at the following address: https://github.com/dfsantamaria/DL4xD-Reasoner. 2
The input of the reasoner is an OWL ontology, serialized in the OWL/XML
syntax (see Figure 1). If the ontology meets the DL4D; requirements, then a
parser produces the internal coding of all axioms and assertions of the ontology
in set-theoretic terms as a list of strings. Such translation exploits the function
used in [
KB. Subsequently, a KE-tableau TKB, representing the saturation of KB, is
constructed according to Procedure saturate-DL4D; -KB in [
PB-Rule We rst show how the internal coding of DL4D; -KBs represented in terms of 4LQSR is de ned and how data-structures for the representation of formulae, nodes, and KE-tableaux are implemented. Then we describe the most relevant functions that implement the algorithm.
4LQSR elements such as variables, pairs, relators, logic connectors, and quanti ers are internally mapped as strings.
The class Var describes 4LQSR variables by means of a string representing the name, an integer representing the sort of the variable, and an integer indicating whether the variable is bound or free. Purely universally quanti ed variables and free variables are collected in the vectors VQL and VVL, respectively, which provide a subvector for each sort of variable.
The operators admitted in 4LQSR and internally coded as strings are mapped in three distinct vectors that are elds of the class Operator.
4LQSR atomic formulae are stored using the class Atom. The latter has two elds: the integer atomOp representing the operator of the formula, and the vector components, whose elements point to the variables involved in the atomic formula. 4LQSR formulae are represented by the class Formula having a binary tree-shaped structure, whose nodes contain an object of type Atom. The left and the right children contain the left and the right subformula, respectively. The class Formula contains a pointer to an object of Atom, representing the atomic formula.
The KE-tableau decision procedure exploits the class Tableau. This class uses the instances of the class Node that represents the nodes of the KE-tableau. Node has a tree-shaped structure with four elds: a vector of Formula that collects the formulae of the current node, and three pointers to instances of the class Node that are the left, the right, and the father node. The set of open branches is collected in the eld openbranches, whereas the set of closed branches is maintained in the vector closedbranches. In addition, the class Tableau is provided with a three-dimensional vector of integers EqSet, which stores the equivalence classes induced by the atomic formulae of type X0 = Y 0, for each branch # of the tableau and for each variable in # occurring in any atomic formula of type X0 = Y 0.
The task of parsing the ontology from the OWL/XML le is performed by the function readOWLXML. The latter takes as input the string obtained by reading the OWL/XML le and returns a vector of strings representing the internal coding of the KB. Once all input formulae have been parsed, the reasoner constructs the expansion of the KB by means of the procedure expandKB, which yields the vector of the output formulae (out) from the vector of the input formulae (inpf). In order to instantiate all the quanti ed variables, expandKB exploits a stack and the vectors VVL and VQL. After this step, the reasoner checks for atomic clashes in the expanded KB by means of the procedure checkNodeClash.
The construction of the KE-tableau is performed by procedure expandTableau, which exploits two stacks of type vector of pointers to Node. The stack noncomBranches, keeps track of the non-complete branches, while nonfulFormula keeps track of the non-ful lled disjunctive formulae. Initially, expandTableau attempts to empty the stack nonfulFormula by selecting iteratively its elements and applying either the procedure ERule or the procedure PBRule, respectively implementing the E-Rule and the PB-Rule in Figure 2. The disjuncts of the current formula are stored in a temporary vector and selected iteratively. If a disjunct has its negation on the branch, it is removed from the vector. Once all disjuncts of the formula have been selected, if there is only one element in the stack, then the procedure ERule is applied to the disjunctive formula. If the stack contains more than one element, then the procedure PBRule is applied. Finally, if the stack is empty, a contradiction is detected, and the branch is added to closedbranches. The procedure expandTableau terminates when either noncomBranches or nonfulFormula are empty. When the procedure terminates with some element in noncomBranches, such branches are added to the vector openbranches. The subsequent phase consists in constructing the set of equivalence classes EqSet for each open branch computed by expandTableau. EqSet is computed by the procedure computeEqT. For each open branch in openbranches, the procedure searches for formulae of type X0 = Y 0, where X0 and Y 0 are selected with respect to the ordering provided by the vector VVL, and, for each variable, stores the equivalence class in EqSet.
The procedure terminates when all open branches of the vector openbranches have been analysed. If the vector is not empty, the KB is declared to be consistent.
We have presented an ongoing implementation of a KE-tableau based decision procedure for the consistency problem of DL4D; -KBs in terms of set-theoretical 4LQSR-formulae. The reasoner, developed in C++, takes as input OWL ontologies serialized in the OWL/XML format.
Currently, the tool is in its beta-testing phase. We plan to compare it with
existing reasoners such as Hermit [