Comparison of Reasoners for large Ontologies in the OWL 2 EL Profile

We like to thank both reviewers for their constructive and helpful comments. We thoroughly and substantially revised the paper, addressing all concerns. Please find the details below.

Firstly, I have noticed that there are sentences (in Section 3.1 even entire paragraphs) taken from published papers of other authors with only minor modifications and no reference to the original source in those places. This lies almost on the border of plagiarism. I realize that the paper is a survey and therefore this is perhaps not too serious, but I still don't think it is acceptable in a respectable publication. I have brought this matter to the attention of the editors.

Response:
We thank the reviewer for pointing us to our inaccuracy. We agree that the way sentences were formulated in the previous manuscript did not pay respect to the sources they came from. We now cited all quotations from published papers and re-formulated sentences from the web where appropriate. An example for an added citation is: Such procedures aim at large expressivity and, according to [24], classify an ontology by iterating over all necessary pairs of classes and trying to build a model of the ontology that violates the subsumption relation between them.

Secondly, it seems that some text was taken directly from the websites of the individual reasoners and the text sometimes doesn't even fit well with the rest of the paper. The descriptions of HermiT and Pellet in Section 4 sound very much like advertisements.

Response:
In order to provide the information that was given by the developers of the reasoners, we used text from their websites with little editing. We agree that outside of the context of a webpage these texts may look like advertisement and have thus re-formulated the descriptions, keeping their meaning but changing their tone. For example, we changed the description of HermiT into: HermiT (University of Oxford) [42] can determine whether or not a given ontology is consistent and identify subsumption relationships between classes, among other features. HermiT is based on a "hypertableau" calculus.

Section 5.1 contains the statement "TrOWL REL implements EL++ without datatypes" even though datatypes were not mentioned when EL++ was introduced on page 5. Similarly, the same paragraph says that FaCT++ doesn't support Top/Bottom Object and Data properties, keys and datatypes (from the FaCT++ website), which I find irrelevant for the comparison since none of these features are needed in the evaluation and are never explained in the rest of the paper.

Response:
We included datatypes when EL++ is introduced in Section 3.1. and removed the statement that "FaCT++ doesn't support Top/Bottom Object and Data properties, keys and datatypes (from the FaCT++ website)" from Section 5.1. as we agree that it is irrelevant for the comparison.

COMPUTATIONAL COMPLEXITY:
The paper seems to misinterpret computational complexity and can mislead readers who are not well acquainted with it. It suggests that the worst-case computational complexity of the language supported by a reasoner is a feature that has an immediate effect on the performance. Section 3.1 says roughly "worst-case behaviour occurs rarely in practice but, nevertheless, it can occur". It is perfectly possible that a reasoner for SHIQ or SROIQ terminates in polynomial-time on all EL ontologies. CB implements an extension of the standard EL algorithm, so on EL ontologies it behaves (in theory) exactly like CEL. Tableau reasoners use specific optimizations that can ensure polynomiality when the input is in EL. The conclusions of Section 5.4, i.e. that there is almost no trade-off between the expressivity of the supported language and the classification performance on EL ontologies, are therefore much less surprising than indicated.

Response:
We thank the reviewer for this comment. We adapted the paragraph on computational complexity in Section 3.1 to make it more clear that worst-case complexity does not have an immediate effect on the performance, especially with EL ontologies as input. Also, we changed the wording on our conclusions of Section 5.4. by deleting the word "Interestingly, so that they do not suggest any longer that the results are surprising.

SOUNDNESS AND COMPLETENESS IN PRACTICE:
In my opinion, most of the material on page 14 (and in Tables 10 and 11) is irrelevant for judging correctness of reasoners. It can all be summarized by saying that there is no standard specification for outputting the class hierarchy, some reasoners output several tautologic axioms, and therefore one cannot compare their outputs line by line. I don't think it is necessary (nor interesting for the readers) to repeatedly discuss the differences between the reasoners and the exact numbers of particular axioms for every test ontology.

Response:
We fully agree on this comment. We compared the outputs of the reasoners line by line, but for the reader a short summary is much more interesting. Thus, we significantly shortened this section and removed Table 10 and 11.

Also, the statement "all included reasoners are sound and complete for OWL2 EL in theory and (their next versions) also in practice" in the conclusion of the paper is too bold and not even correct. Firstly, there are features in OWL2 EL (e.g. datatypes) that are not in EL+ nor in Horn SHIF, so according to Table 2 at least CEL, SR and CB are not complete for OWL2 EL even in theory. Secondly, one can never do enough testing to prove that a program is correct in practice. All three test ontologies are in EL+ which covers only a subset of OWL2 EL, so some features of OWL2 EL were not tested at all. Furthermore, it is a bit naive to believe that a new release of an incorrect reasoner will fix 100% of its bugs.

Response:
We thank the reviewer for this comment. It is true that the statement in the conclusion is too bold and not even correct, so we removed it. We agree that one can never do enough testing, and added to our conclusions that "Ongoing testing is necessary to evaluate the correctness of reasoners in practice.".

ERRORS, TYPOS
- Section 3.1, Soundness and Completeness in Theory: There are two different definitions of correct in the same paragraph (correct = sound, correct = sound and complete).

Response:
--------
We corrected this and now use only the later definition correct = sound and complete.

- Table 1: You should spell out that the table shows complexities of concept satisfiability checking and not for example of concept subsumption checking.

Response:
We added this comment to the accompanying text and to the table caption.

- page 5: "nominals with one individual" is tautological. A nominal is always a single individual.

Response:
Right, we removed "with one individual".

- Table 2: Pellet's explanation should have "Fracture of lower limb" instead of "Fracture of bone".

Response:
Thank you, we changed it.

- Section 4: Does CB support Horn SHIQ or Horn SHIF? The text says the former but Table 2 shows the latter. Anyway, none of these is an extension of the full EL++.

Response:
We clarified this issue by adding: CB's reasoning procedure described in [24] supports Horn SHIQ, but its implementation supports only Horn SHIF, which is a subset of Horn SHIQ that does not include cardinality restrictions. We also changed the wording in 5.1. into "Most reasoners rely on tableau-based methods or on (extensions of) completion rules for EL."

- everywhere: FaCT++ is sometimes spelled as Fact++, sometimes as FacT++, sometimes just as FaCT

Response:
We spell it now everywhere as FaCT++, only two times as FaCT: once in the section on FaCT++ (FaCT++ "is the new generation of the OWL DL reasoner FaCT") and once in the literature review (CEL "has been compared to FaCT and Racer in 2005"). The reasoner is also referred to in the cited paper as FaCT without ++, and in 2005 the reasoner was probably not renamed yet.

Solicited review by Julian Mendez:

We thank the reviewer for his positive comments on our manuscript.

There are some minors corrections and observations listed below:

Typos:
> * Page 3, Column 2, Line 37, it says:
> "CB classified SNOMED CT in less then a minute, ..."
> and should say
> "CB classified SNOMED CT in less than a minute, ..."

Response:
Thank you, we corrected this typing error.

Suggestions:
* I suggest to use a different typeset for formulas (e.g. mathsf ), especially when they are part of a paragraph. Examples are in:
> Page 5, Fig 2
> Page 5, Column 2, Paragraph 1
> Page 6, Column 1, Paragraph 1
> Page 15, Fig 3

Response:
We agree and use a different typeset (textsl) now.

* I consider that:
Page 6, Column 2, Line 10, where it says:
"Protégé-4" should say "Protégé 4".

Response:
We changed that, too.

Clarifications:
I did not understand the following sentences:
* Page 4, Column 2, Line 13, it says:
"It is important to know whether a reasoner is sound and complete, but not always important that it is sound and complete."

Response:
We want to express that the user can gain speed by giving up soundness or completeness. In a scenario where speed is the main criterion, a reasoner might not have to be sound or complete, as long as it is fast. We believe that it is always important for a user to know how the reasoner behaves. We re-formulated the section so that it is more clear now: "Soundness or completeness can be sacrificed for a significant speed-up of reasoning [41]. Thus, to employ a reasoner in a real-world application, it is not always important that its underlying reasoning method is sound and complete, but it is important to know whether it is sound and complete.

* Page 7, Column 2, Line 40, it says:
"Horn SHIQ ontologies are ontologies expressed in the DL SHIQ, which do not contain 'non-deterministic' constructors, ..."

* Page 8, Column 1, Line 29 it says:
"The main aspect of this algorithm is that is less non-deterministic that other ..."

Response:
As we agree that it is unclear what "non-deterministic" means, and as it is irrelevant in our context, we removed both sentences.

I did not understand the purpose of Table 11.

Response:
As mentioned in a response to the first reviewer, we removed the table. We agree that it was irrelevant in the scope of this paper.