Ontologies are a powerful tool of knowledge representation, which became very popular for using by expert systems [8]. First of all because of the fact that they are based on the description logic formalism, which has a formally defined semantics allowing to develop tableau algorithm for a logic inference. OWL [13] is the basic ontology representation language recommended by the W3C consortium. Nowadays the OWL 2 standard is valid. The OWL DL language uses the SHOIN [1] description logic with support of data values.
To date many OWL reasoning systems such as FaCT++ [15], HermiT [7] (for OWL DL), jcel [11], ELK [10] (for OWL 2 EL) were developed, they implement different algorithms for a logic inference.
The article introduces a new OWL Reasoner. The TReasoner is SHOIQ(D) reasoner implementing tableau algorithm with some novel optimization techniques. TReasoner is free distributed by GNU General Public License v2. Source code of the TReasoner, compiled class library and wrapper for system usage are available at http://treasoner.googlecode.com.
This system description has the following structure. Section 2 provides a supported language and an implemented algorithm. Section 3 contains information about architecture, implementation and optimization techniques that are used by the TReasoner. Results of the system testing are described in section 4. Section 5 concludes this work.
Reasoning Algorithm
The TReasoner allows to perform a concept satisfiability checking, a consistency checking and a classification on OWL ontologies that use the SHOIQ(D) description logic. It means that the system works correctly with concepts described by the disjunction, the conjunction, the existential quantifier and the universal quantifier. Besides, the SHOIQ allows roles to be transitive and inverse to other roles. There may be concepts consisting of one individual (nominal), at the same time the SHOIQ is extended by number restrictions (n ≤ R.C or n ≥ R.C). D letter at SHOIQ(D) logics allows to describe knowledge with support of datatypes (strings, numbers, dates and etc.). The TReasoner implements the tableau algorithm [6]. The concept satisfiability checking is carried out through graph-model existence checking.
The tableau algorithm for SHOIQ has NExpTime complexity, but the developed system implements different new and old optimization techniques, which allow to significantly reduce worktime in practice.
The TReasoner was developed using the Java language, because of the crossplatform portability. The system consists of 6 packages. The RuleGraph package implements data structures for the inner representation of concepts. Also this package implements algorithms for the concepts simplification and the axiom simplification. TBox, ABox and RBox axioms are contained in KnowledgeBase package classes. The OWL API package is used for loading the OWL ontologies and transforming them to inner system representation. Main package is Checker. It contains classes that implement tableau algorithm and optimization techniques for it. Checker package classes use Interpretation package classes, which implement data structures for the interpretation building. All packages use classes of the Help package, which implements different supporting algorithms and data structures such as binary heap, hash-table, etc. The UML package diagram is presented on the Fig. 1.
The TReasoner implements optimization techniques, which can be divided into 3 groups: 1. Preprocessing optimizations; 2. Tableau algorithm optimizations; 3. Classification optimizations.
The system uses both time-tested and newly developed optimizations.
Preprocessing optimizations are used by the ontologies transformation to inner structures, which are understandable by the TReasoner. Also they are used for the transformation of GCIs and equivalence axioms. For the concept representation the system uses direct acyclic graph (DAG), each vertex of the graph corresponds to some operation or quantifier, and neighbours of this vertex are operands of the operation, in addition each vertex in the DAG has a number that uniquely identifies it. To reduce memory usage, same concepts are represented by only one subgraph. For each vertex (in order of height increasing), a hash-function value is calculated, this function consider unique numbers of all neighbours, operation type of the vertex, unique number of a role and number restriction (for existential and universal quantifiers, and for number restriction operations). If this function value doesn't exists in hash-table, the vertex with its hash-function value will be added to hash-table. If function value is found then all edges which enter to this vertex will change its direction to vertex with corresponding value of hash-function that contained in hash-table.
To reduce memory usage, removal of brackets technique was developed. The algorithm is performed in two runs. In first run, for each vertex v (in order of height increasing) that represent a concept, set of concepts H(v) is calculated. Concepts of this set defined as follows: In second run, vertexes are considered in order of height decreasing, each vertex is transformed to -vertex with neighbours of all concepts from H(v) and itself vertex, so each concept of H(v) will be deleted from H(u i ) for all u i which are neighbours of v. For example, concept ((
After loading and preprocessing of concepts, a processing of axioms will be performed. Absorption technique [5] is used for this task.
Tableau algorithm optimizations that are implemented in the TReasoner, include such optimizations as backJumping [14], caching [3,5] and global caching [12]. The system implements novel optimization techniques. The main of such techniques is the SS-branching [9], which determine disjointness of concepts without using of tableau algorithm. It is applicable not in every cases, but in wide range of concepts. The SS-branching procedure determine disjointness of two concepts by analyzing of structures of DAGs that represent its. For example, if concepts C and D are conjunctions of other concepts
) and some of the concepts C i and D j are disjoint, then C and D are disjoint. Conditions of disjointness for cases when C and D are disjunctions, disjunction and conjunction, existential and unversal quantifiers were identified. However, SS-branching can not to determine disjointness of concepts. To cover wider class of concepts Bron-Kerbosch algorithm was used. For disjointness checking of the concepts like E 1 E 2 ... E n , where every concept E i is a disjunction (E I ≡ F 1 F 2 ... F k ). Such concepts will be presented of n-partite form, where every vertex of the part presents F j concept, so vertexes form different parts will be connected, if corresponding concepts are disjointness. Model existing checking of such concepts performed by using of Bron-Kerbosch algorithm, which used for n-clique finding in n-partite graph.
Classification optimizations allow to reduce system worktime to perform the classification operation. Enhanced traversal method [2] is used for the classification, information about disjointness is extracted not only from subsumption test, but during the concept satisfiability testing. During the construction of model by tableau algorithm, labels of all individuals are checked in the presence of concepts A and ¬B, though A and B are concept names. If those individuals exist, then A B, without performing A B subsumption test.
The TReasoner system performance testing uses ontologies classification tests that were used on the OWL Reasoner Evaluation Workshop 2012 and compares the results received by HermiT (ver. 1.3.6) and FaCT++ (1.6.2) reasoners. They implement hypertableau and tableau algorithms and support the SROIQ(D) logic. Information about used ontologies is shown in table 1.
System testing results in comparison with other reasoners are shown in table 2. First column of the table contains name of used ontology, and every subsequent column shows time spent for ontology classification by the relevant system. Testing was carried out on ASUS Notebook VX7SX Series Intel Core i7-2630QM CPU@2.00 GHz 2.00 GHz; 6.00 GB RAM running under Windows 7. The resulting classification coincides to the reference classification provided together with chosen ontologies.
This system description presents the new reasoning system, implemented algorithms and implemented optimization techniques, which contribute to reduce worktime of different ontologies operations (classification, concept satisfiability checking, consistency checking). The developed system allows to perform logical analysis for expressive SHOIN (D) logic that is used in OWL DL. This fact allows to use TReasoner to perform operations on a wide class of ontologies.
The presented testing results show that TReasoner may not compete yet with most popular systems such as HermiT and FaCT++ reasoners, but in future implementation of tableau algorithm will be improved and reduce of system worktime is expected.
In further researches improving of the TReasoner is expected in order to use it not only as module of the enterprise architecture verification expert system, but as self-dependent OWL reasoning system.