We present a survey of the current OWL reasoner landscape. Through literature and web search we have identi ed 35 OWL reasoners that are, at least to some degree, actively maintained. We conducted a survey directly addressing the respective developers, and collected 33 responses. We present an analysis of the survey, characterising all reasoners across a wide range of categories such as supported expressiveness and reasoning services. We will also provide some insight about ongoing research e orts and a rough categorisation of reasoner calculi.
The utility of reasoner surveys is twofold: the main purpose is to inform users about the systems they can potentially choose from, the secondary purpose is to give an overview of the reasoner landscape, both to reasoner developers and other related researchers. In this work, we focus on the second purpose. Instead of providing a detailed list of reasoners, we group them according to our classi cation scheme and report on commonly exhibited features. We discuss features such as logical services, licensing and supported OWL pro les. Rather than consulting potentially outdated literature, we decided to directly address reasoner developers to ll in a detailed survey involving questions about parallelism, mobile support and use of modules.
Our main contributions are (
There are two main types of reasoner surveys: (
While reasoner benchmarks have recently received increasing attention, for
example in the ORE reasoner competition [13], exhaustive meta-data surveys
and reasoner listings are sparse and rarely comprehensive or up-to-date [29, 39].
The most comprehensive relatively recent study [22] provides an historical
account of description logic reasoners from the early implementations (1975) until
modern OWL reasoners such as HermiT. The authors analysed each reasoner
with respect to four basic aspects: (
Not all reasoners are intended to support the entirety of OWL 2 DL. Reasoners such as HermiT and FaCT++ support all of OWL 2 DL, while many e cient reasoners exist that only deal with tractable pro les of OWL and OWL 2; ELK and CEL are examples of highly e cient reasoners that handle (most of) OWL 2 EL. There are also many reasoners that deal with extensions of classical DLs, such as fuzzyDL, a reasoner for fuzzy extensions to DLs. Amongst this variation are the reasoning services that the reasoners o er; some are very e cient at TBox queries such as classi cation (computing subsumption relations between named classes), whereas others are meant for query answering. From a utilitarian perspective, we believe that supported reasoning services, expressivity levels (including the degree of datatype support) and the completeness of the implemented algorithm are the most important characteristics to categorise a reasoner. A second way to classify the reasoner is by the primary calculus underlying its core reasoning service, for example tableau or consequence-based procedures. This distinction is primarily useful for researchers that are interested in nding more e cient ways to solve reasoning problems. 4.1
Modern OWL reasoners support a number of primary logical services such as consistency, classi cation, instance checking and entailment checking, and secondary services such as explanation for entailments and inconsistency, (semantic) module extraction and ontology based data access (OBDA). Explaining these services in detail is beyond the scope of this survey. It should su ce to say that some reasoners are particularly optimised to operate on concept level (TBox) knowledge, for example o ering an e cient classi cation service, while other reasoners o er the user services for e cient instance retrieval (ABox level), most notably through conjunctive query answering. In our work, we attempted to determine key and ancillary reasoning services for all reasoners participating in our survey.
We de ne the expressivity of a language as the quality and conceptual breadth
of the constructs which make up the language. The expressivity supported by a
reasoner is the most expressive language for which it can provide a key reasoning
service. As such, expressivity is not an attribute of the reasoner, but of a
reasoning service: a reasoner might o er di erent sound reasoning services for varying
levels of expressivity. There are many ways expressivity can be documented and
communicated, for example: (
In general, a sound algorithm will never answer Y ES if N O would be true and a complete algorithm will never answer N O if Y ES would be true. For example, given an algorithm P , an ontology O, and an axiom over O of the form A v B where O j= , P (O; ) says YES i O j= , where soundness is the ! direction and completeness is the direction. Both can be seen as important and required characteristics of a reasoner. To show why, a trivial implementation of a sound and incomplete algorithm answers N O to every question, where as a trivial implementation of a unsound but complete algorithm answers Y ES to every question - both can be seen as irrelevant if not taken together. While it would make sense to classify each reasoning service individually on whether the underlying algorithms are sound and complete, we simplify our measurement to determine what the algorithm underlying the key reasoning service is. In our survey, we distinguish broad categories of completeness, but assume that all procedures are generally sound. 4.2
We identi ed 3 main categories of calculi: consequence-, model construction- and rewriting-based. In general, consequence-based reasoners rely on adding logical consequences (entailments) to a knowledge base (KB) without the need to check possible consequences that are not entailed by the knowledge base. This category covers similar techniques such as resolution-based techniques, rule-based procedures and completing algorithms. These techniques are most commonly employed for reasoners that deal only with the fragments of OWL 2 DL such as EL+ and EL++, and are used by some popular reasoners such as ELK and CEL. Model construction techniques are based on building models based on the KB and checking for KB consistency. These are generally utilised for quite highly expressive fragments of OWL 2 DL, i.e. those extending ALC. This category includes those reasoners that use automata-based approaches, tableau and hypertableau techniques. Rewriting is a technique used to expand a KB by rewriting the facts of the KB, to be used for a speci c task, e.g. query answering, making the reasoner less reliant on the terminological aspect and more involved in the data aspect. This technique is most commonly used for query rewriting and catalogue rewriting but can also be used for structural transformation of a KB.
While we attempted to determine which calculus was primarily employed by the reasoner developers, there seems to be a trend, at least for the general purpose reasoners that cover the entirety of OWL 2 DL reasoning, to employ hybrid techniques, for example combining saturation-based or consequence-based techniques with tableau-style techniques (Pellet, Konclude, WSClassi er and others).
The subjects of this survey are current, stand-alone reasoners that can deal with OWL. We de ned current as either being updated or published over since January 2012. Being able to deal with OWL means that at least one of the standard reasoning services above was supported on a de ned fragment of the OWL. Stand-alone means that the reasoner is meant to be used by itself, rather than being a dependent component of a bigger system, such as the various inference engines as part of triple stores.
This survey emerged as a by-product of a systematic review on DL reasoning system evaluation quality. It is however by itself not strictly systematic. The initial list of reasoners was created from publicly maintained lists [29, 39]. More reasoners were found through respective Google searches. This knowledge directly informed the search strategy for the systematic review mentioned before, which again yielded a large range of system description papers that lead to amending the full list of reasoners. After the search was completed, our list included 68 description logic and OWL reasoners, with another two being added later as part of a feedback round from reasoner developers.
As a rst step, we attempted to nd evidence of use of each reasoner by searching Google and Google Scholar for web pages that led to version control systems or other kinds of download pages as well as academic papers. We recorded the most up to date evidence we could nd (for example, the latest commit in a version control, the publication date of the most recent paper). If a reasonable attempt at nding evidence failed (repeated searches with varying keyword combinations, references in perhaps older system description papers), we excluded the reasoner from the survey. Apart from the 35 reasoners we mention in this survey, the original list contained the following reasoners: COROR, RacerPro, *SAT, BACK, CB, Cerebra Engine, CICLOP, CLASSIC, Condor, CRACK, DLP, Fact, FLEX, HAM-ALC, K-REP, Bossam, KRIS, LOOM, MSPASS, QuOnto, SHER, YAK, OWLGres, Pronto, DLEJena, F-OWL, Fresg, OWLer, OntoMinD, Screech, REQUIEM, YARR!, Kaon2, Elly and SoftFacts. Most of these reasoners are quite old description logic reasoners, some reasoners, such as RacerPro, are superseded by other reasoners (Racer). For none of these reasoners we were able to nd proof that they were used or published about since January 2012. The YARR! reasoner did have a workshop paper in 2013 [30], but we decided to exclude it from the survey because we were unable to nd a more substantial proof of existence (like a web page). We sent our survey to the developers of the remaining 35 reasoners.
The survey itself was implemented as a series of questions in SurveyMonkey1, as a joint e ort of a team of experts including reasoner developers, logicians and
empirical researchers. The results were used to update the popular reasoner listing2 at Manchester. 6
Out of the 35 surveys sent out to reasoner developers, we collected 33 complete answers. Surveys for OwlOntDB [10] and Deslog [40] were not completed at the time of this writing. An overview of all participating systems can be found in Table 1 (see appendix). As discussed in the introduction, we do not aim to provide a discussion of the individual reasoners. Additional information can be found on the Manchester University pages mentioned in the previous section. 6.1
As can be seen in Figure 1, the majority of reasoners were developed in the last ve years (23 out of 33). However, 3 reasoners have been around for more than ten years, all of which have been updated during the last two years. 23 are actively developed, 8 are merely maintained (bug xes etc.) and two reasoners, CEL and HermiT, are not maintained at all anymore. In terms of implementation, most reasoners are based on the Java programming language. This is not surprising, given that the dominant frameworks supporting OWL, such as the OWL API [16] and Jena, are implemented in Java. As can be seen in Figure 2 there are, interestingly enough, a good number or reasoners implemented in other languages though, such as the more e cient C/C++ or Prolog. More than two thirds of the reasoners in the set implement the OWLReasoner interface of the OWL API. Like other questions in the survey this one was optional, thus merely establishing a lower bound, but it already demonstrates the ubiquity of the framework. The majority of reasoners are accessible via the command line, or are readily available for integration with the Protege editor, also Figure 2. The dominant underlying primary calculus is tableau (10 out of 33), but only just. It is inherently di cult to classify modern reasoners accurately. Konclude for example uses a hybrid approach that involves tableau and some nested saturation-based techniques. Many full edged OWL 2 reasoners come with an e cient consequence-based delegate reasoner for EL ontologies, such as Pellet, FaCT++ or WSClassi er. For this survey, we grouped the di erent techniques into the categories described in Section 4.2. As can be see in Figure 2, most reasoners are primarily based on an approach that involves model construction.
Few reasoner developers report to make use of modularity, perhaps surprisingly. Only four reasoners, including full edged modular reasoners such as MORe and Chainsaw, report to make use of modularity for classi cation, and only three reasoners (Pellet, FaCT++ and DistEL) are reported to make use of modularity for incremental reasoning. Only 6 reasoners are known to draw on parallelism to improve classi cation performance, and only 4 mobilise it during pre-processing. Up until today, little is known whether parallel techniques like 2 http://owl.cs.manchester.ac.uk/tools/list-of-reasoners/ 2015 2010 s r a eY2005 2000
0 20 15 10 5 0 Last Update Prototype Launch 10Reasoners (ordered by prototype launch date) 20
30 parallel or-branching or parallel module classi cation actually do much good, especially for tableau-style reasoning. Three reasoners, CEL, snorocket and WSClassi er have been reported to be tuned to particular ontologies (SNOMED CT the two former, a version of FMA the latter). Given the growing interest for mobile technology, we also asked whether the reasoner has been run on a mobile device. 5 reasoners where run on Android (ELK, JFact, jcel, LIFr, BaseVIsor), 24 where never run on a mobile device and for 4 reasoners the developers did not give an answer. Some reasoners do not merely provide reasoning services for standard description logics. A minimal support for the most important extension, datatypes, is provided by many reasoners. In our survey however, 16 reasoner developers did not give any indication for datatype support. Full support of all datatypes on the OWL 2 datatype map is reported for 6 reasoners. The question was optional, however, so the numbers have to be interpreted cautiously. Other prominent extensions are fuzzy with 3 reasoners, probabilistic with 4 and distributed reasoning with 2 reasoners in the survey. Multiple extensions to standard description logic (for example distributed-fuzzy) reasoning do not seem to occur at all.
As was discussed in Section 4.1, we will report the supported language expressivity in two ways: Supported OWL pro le and the main underlying description logic family. Both can be seen in Figure 3. For readability, we have grouped the DL languages into 3 rough categories: Horn-style languages includes EL, RL, Horn-SHIQ and similar. Horn logics are those that provide no means to express any form of disjunction, either directly or indirectly. They do not require any form of \reasoning by case", often have nice canonical models, and are generally suited for consequence-based reasoning. To the right of the gure, we summarize the degree of completeness of the underlying algorithms. SC stands for soundness/completeness, SI stands for sound and incomplete, SC/Pro le means that the reasoner is sound and complete for one of the pro les, SC/OWL1 sound and complete for OWL 1 and so on. Only six reasoners in the set are incomplete, and the majority of reasoners are complete at least for one of the polytime OWL pro les. This is also consistent with the supported pro les: The majority of reasoners support OWL 2 EL, and at least 12 reasoners are directly recommended for the OWL 2 EL pro le (see questionnaire).
15 10 5 0
Most reasoners support simple satis ability checking (22 out of 33),
knowledge base consistency (
We hope that our work will inform reasoner developers of other relevant projects in their eld, and support them to get a sense of the coverage and directions of current reasoner development trends. We tried to get an idea of (intended) use for concurrent or parallel technologies, as well as modules. The survey we conducted covers many more aspects than we could report on within the limits of this paper. We asked for supported datatypes individually, employed reasoner optimisations and recommended usage. The resulting data will form the starting point for a knowledge base about reasoning systems and ontologies. We have already started working on an OWL reasoner ontology (ORO) that attempts to model language expressivity, calculi and reasoner optimisations in a ne grained fashion, to serve as a schema for the knowledge base. ORO is directly informed by the outcomes of this survey and is, in its very prototypical rst version, available online3.
Matentzoglu et al.
Name Institution SC ACT CALC BaseVISor[19] VIStology, Inc. P B Rete Network BUNDLE[27] Univ. of Ferrara O2 D Tableaux CEL[2] Technische Universitt Dres- P N Consequence-based den Chainsaw[37] Univ. of Manchester O2
Clipper[9] Vienna Univ. of Technology P DBOWL[11] Univ. of Malaga O1 EXP
NA SROIQ
EL+
SROIQ Horn-SHIQ
SHOIN D Modular Reasoner B Query Rewriting D Relational Algebra and xed-point iterations D Fuzzy D Consequence-based D Compressed models D Tableaux D Hybrid D Hypertableaux D Query Rewriting D Modular Reasoner D Query Rewriting D Tableaux B Tableaux D Datalog Rewriting D Datalog Rewriting D Consequence-based B Tableaux D Tableaux D Tableaux D Consequence-based B Hybrid