When one Logic is Not Enough: Integrating First-order Annotations in OWL Ontologies

This paper presents Gavel-OWL as a valuable tool that provides a practical way to extend OWL with FOL axioms. The paper is well organized and easy to follow and the tool is available and well documented on github. The capabilities and the functioning of the tool are well explained, the approach of FOWL annotations is fairly easy to use and has the potential to be widely adapted by the community. The results from the tool's evaluation showcase its benefits. So overall an excellent paper that I would like to see published.
My biggest concern (and the only reason I choose “major revision” rather than “minor revision”, however, is Section 4.3. While I certainly see the use and interest in this part, up to 11:32 it seems quite disconnected from the remainder of the paper. It goes very deep into the specifics of SMILES strings and -- depending on the specifics of the class of molecules -- how they lead to different kinds of FOL axioms. But at the same time, without even more details (like the templates used to produce the FOL annotations), I don't know what to take away from this part. Because the generation of the FOL annotations doesn't relate much to the Gavel-OWL tool, I think it might be better to take this part out and save it for a separate paper that focuses on the FOL annotations for ChEBI. You could still leave the experimental part (from 11:32 on) in as it still shows how the FOL annotations are useful to prove things that the ontology cannot prove. But the unexpected counter-examples seem to point more to a problem concerning SMILES annotations than OWL, so I'm not sure how relevant it is to the evaluation of Gavel-OWL.
If you choose to keep it in, it needs to be presented in a way that shows the fuller picture (especially the templates used to translate SMILES annotations) but is still accessible to readers who don't know much about chemistry or ChEBI.

Apart from the Sec 4.3 there are a few additional issues that should be fixed in the final version:
1. I believe that the divide between FOL ontologies (as used for foundational ontologies) vs. OWL ontologies needs some solution and that the proposed approach makes sense. But there is another approach to pursue this by keeping only an FOL ontology (as authoritative version) and extract OWL versions from them. This alternative approach is outlined in Hahmann & Powell 2021: Automatically Extracting OWL Versions of FOL Ontologies, Proc. of ISWC 2021, https://doi.org/10.1007/978-3-030-88361-4_15 should be acknowledged. I assume you may simply not have seen it yet.
Even for existing OWL ontologies, this approach would be equally feasible if one first translats the OWL ontology to FOL (which is straightforward and you're already doing) and then adding the FOL annotations as axioms.

2. 5:19: The best citation for Macleod is actually the 2021 ISWC paper mentioned above.

3. 10:Listing 2: requires more explanation for those unfamiliar with the SMILES notation (i.e. does # indicate a triple bond?, where does the "has_no_charge" come from?) Showing the template used to generate this axiom may help.

4. 10:46-51: how would you express that in FOL? It seems very cumbersome (not to speak of being unreadable). OWL-DL seems better at expressing the cardinality constraints.

5. 11:3ff: the formalization of the second category as individuals seems reasonable at first sight but may lead to unintended consequences when defining, e.g., mixtures (any mixture of water and something else would then say that they contain the same water molecule). Seems to equate the material water with a water molecule.

6. 11:31 When you say that ChEBI is inconsistent, what do you mean? That it is inconsistent with its FOL annotations? Or by itself?

There are also some limitations that I feel should be discussed more explicitly in the paper (potentially in a future work section):

7. CLIF and TPTP (as FOL in general) allow the use of function symbols in addition to predicates, whereas OWL only allows declaring a property as functional, this is not quite the same. So there may be OWL properties restricted by FOL axioms that use a function symbols. How is the mapping established? Are such OWL properties converted to FOL functions to facilitate the reasoning? Or is everything treated as a predicate?

8. A question about the underlying mapping between OWL and FOL: are all OWL cardinality constraints expressed in FOL? They can become quite cumbersome.

9. How are OWL imports dealt with? Are they extended to FOWL to facilitate the reasoning?

The paper presents Gavel, a tool which supports developing and reasoning over ontologies written in FOWL, a first order extension of OWL. Gavel provides an Protege extension which allows the user to add FOL axioms to OWL ontologies and it performs reasoning over such heterogeneous ontologies by translating all data to TPTP and then executing it in a theorem prover. The authors describe their implementation and show various examples for which the addition and/or evaluation of FOL axioms to OWL ontologies provide an added value.

As such, the paper is well written and very interesting. I also think that there are OWL use cases that could benefit from the addition of FOL formulas. However, I still see two problems with the paper and the approach:

Firstly, the authors do not even mention that OWL-DL is designed for the Web and that many design decisions like for example the use of IRIs reflect that. So I wonder, what happens if we combine FOWL ontologies with really similar FOL annotations which refer to different contexts (think for example in some concept “name” which relates to a foaf:name in one ontology and to some ex:name in another). How do we combine and exchange FOWL ontologies in general? Also: the representation of the FOL formula in a literal might ensure compatibility with OWL, but it also makes it difficult for other standards and implementations (e.g. SHACL, N3, …) to access this data in order to (partly) perform FOL reasoning as well.

Secondly, I would like to learn more about the concrete mapping. The authors provide a link, but did they also formally show the correctness of the mapping? Does the mapping preserve equivalence and non-equivalence.

Most likely, the authors only forgot to add references to address my second problem. Therefore, I am more concerned about the first one and would like to see at least some considerations of the Web-aspect of OWL. But I think, a short discussion treating these issues can be easily added. I therefore recommend a minor revision.

Some more comments:

- Figure 1: the second clif expression denotes symmetry while it should be antisymmetry in order to get a strict order? Maybe I misinterpreted the expression?

- Introduction: you claim that OWL-DL is easier to understand for users than FOL
(CLIF, TPTP). Of course that claim is subjective, but I doubt that given for example that restriction posed on the axioms which are just there to ensure decidability. I would instead add as an advantage the compliance to Semantic Web principles.

- If you do OWL reasoning via Gavel-OWL, do you also have a mapping from (restricted) FOL to OWL to give back results?

- page 9 end, there seems to be a wrong full stop (“. and used…)

- related work: you discuss the problem that OWL-DL combined with swrl is not decidable and that therefore dl-safe swrl was introduced. After that, you talk about swrl+owl which is less expressive than FOL, do you refer to dl-safe swrl or general swrl in that sentence? I am also confused y the wording of the paragraph, since the lack of decidability is presented as a problem while it is clear, that FOL is also not decidable. So how is that part meant?