**The Maximality of OWL-Time**

**Author(s):** Michael Gruninger, Megan Katsumi

**Full text:** submitted version

**Abstract:** Selecting an ontology representation language presents a major challenge due to the trade-off between expressiveness and decidability.

his leads to the question of the relationship between a full first-order axiomatization of an ontology and its OWL2 counterpart –

is the OWL2 ontology really the maximal subtheory of the more expressive first-order

ontology which can be axiomatized in OWL2?

In this paper we consider the relationship between OWL-Time and its first-order axiomatization as

presented by Hobbs and Pan.

We leverage previous work on the verification of the first-order axiomatization of OWL-Time

to propose a novel technique for identifying its maximal OWL2 definable subtheory.

The results show that OWL-Time is in fact not maximal with respect to the first-order axiomatization. We discuss how this approach might be applied to achieve similar results in other areas.

**Keywords:** ontology; OWL; first-order logic; time; ontology mapping

**Decision:** reject

**Review 1 (by anonymous reviewer)**

(RELEVANCE TO ESWC) The general problem addressed by submission is quite interesting: given a first-order theory modeling a domain of interest, find an OWL 2 ontology that captures the maximal subset of the first-order theory. The authors concentrate on a fragment of an early version of OWL-Time and identify two axioms missing in the "current" approximation of OWL 2. (NOVELTY OF THE PROPOSED SOLUTION) The problem of finding equivalent formulas is nothing new in logic. Taking account of different syntaxes does not add very much. (CORRECTNESS AND COMPLETENESS OF THE PROPOSED SOLUTION) Some of the proofs use dubious arguments: for example, the proof of Lemma 1 refers to the syntactic restriction on SRIQ ontologies - yet, no-one says that the same semantically defined property cannot be expressed using another choice of axioms. The proof of Lemma 4 appear to use some unclear arguments. The proof of [Lemma] 5 contains wrong statements: Point <= (\leq n) in.X, Line <= X does not imply P <= \leq n in. Line (did the authors mean X <= Line?). Also, Point <= \geq m in.X \sqcup \leq n in Z is NOT equivalent to Point \sqcap \geq n in.Z <= \leq m in.X. Taking into account that the proofs are not very technical and do not involve any non-trivial ideas, it is just too many typos (or errors). (EVALUATION OF THE STATE-OF-THE-ART) The evaluation of the state-of-the-art is irrelevant. (DEMONSTRATION AND DISCUSSION OF THE PROPERTIES OF THE PROPOSED APPROACH) The notion of ontology equivalence and conservative extensions is well-studied. More related work could be discussed. (REPRODUCIBILITY AND GENERALITY OF THE EXPERIMENTAL STUDY) N/A (OVERALL SCORE) **Short description of the problem tackled in the paper, main contributions, and results** Given a first-order theory modeling a domain of interest, find an OWL 2 ontology that captures the maximal subset of the first-order theory. The authors concentrate on a fragment of an early version of OWL-Time and identify two (functionality) axioms missing in the "current" approximation of OWL 2. SPs 1. The problem is interesting. WPs 1. The results are weak: the two axioms identified for OWL-Time are hardly worth the machinery. 2. The proofs contain a significant number of typos / errors. 3. The proofs appear to be rather straightforward, but quite poorly written: trivial steps like equivalence of \neg \leq n and \geq n +1 are excessively verbose, yet the overall structure of the arguments is unclear. SRIQ is not a profile of OWL 2 - it's a DL (and its typesetting is wrong in all places but one on page 2 and one on page 3). Definition 2: equivalent *to* Footnote 4: constants are irrelevant for SRIQ TBoxes; Sigma(T) is defined here but used above (page 3) Id on page 5 is never explained. Definition 9 appears to miss \exists R.Self. Referring to weak_bipartite.owl in Lemma 1 is a bit unexpected - would it be that difficult to list the axioms in the submission? One has to figure out the order of classes in Figure 1 (a comment, or better labels of the pictures might have helped). Missing upper limits in Definition 11 - are they \infty? I acknowledge reading the rebuttal, which did not really clarify any of the issues.

**Review 2 (by Leo Obrst)**

(RELEVANCE TO ESWC) The paper has strong relevance to the conference insofar as it provides a coherent methodology that a particular subset of the audience (those concerned with ontologies, and in particular, the relationship between a given FOL ontology and its OWL2 less expressive translation) will find value in this. (NOVELTY OF THE PROPOSED SOLUTION) The paper proposes a meaningful methodology for evaluating whether a given less-expressive OWL2 ontology counterpart to a first-order ontology is maximal or not. This methodology, especially when generalized to other such ontologies beyond the exemplary OWL-Time, constitutes a way to consistently (and possibly automatically, given more advanced reasoning systems and ontology tools) compare two or more different OWL axiomatizations derived from a first-order axiomatization. The methodology is fairly general. (CORRECTNESS AND COMPLETENESS OF THE PROPOSED SOLUTION) Although the presentation of the formal correctness and completeness of the given definitions, theorems, lemmas, and proofs appears sound, there are a couple of potential improvements that could be made. E.g., on p. 3, the notion of "incident" (a notion at the core of bipartite incidence geometries) could be better defined in English. This is not obvious to a reader not already familiar with the notion, requiring offline gaining of familiarity with the concept. Similarly, on p. 6, Definition 9 uses "in.C", but this is not defined. Clearly, it is something like "incident of C", but this could be clarified. On p. 7, Definition 11, the crossed circle symbol is used, and is presumably the symbol for the disjoint union according to the text. But this should be clarified. In addition, there is probably too much material relegated external to the paper. (EVALUATION OF THE STATE-OF-THE-ART) A background discussion is provided in the Introduction as to the methods currently used to compare (generate) an OWL2 ontology from a first-order ontology, for reusability, but these are incomplete and prone to comparison errors. Also these do not necessarily ensure that it is a maximal subtheory of the FOL ontology that results in the OWL2 ontology. (DEMONSTRATION AND DISCUSSION OF THE PROPERTIES OF THE PROPOSED APPROACH) Using OWL-Time as an exemplar, the paper defines a methodology which uses maximal OWL2-definable subtheories of the mathematical theories used in verifying an ontology, and then showing how these are preserved by synonomy. The authors define SRIQ-Definable theories, Orderings, Bipartite Incidence structures, and use these (via synonomy preservation) to identify the maximal SRIQ-definable subtheories of OWL-TIME from the SRIQ-definable subtheories of a theory. (REPRODUCIBILITY AND GENERALITY OF THE EXPERIMENTAL STUDY) The experimental study is less empirical and rather more formal. The given formal explanation should enable duplication or assurance that the proofs are correct. However, more of the external material could be incorporated into the paper. (OVERALL SCORE) Summary: The paper proposes a meaningful methodology for evaluating whether a given less-expressive OWL2 ontology counterpart to a first-order ontology is maximal or not. This methodology, especially when generalized to other such ontologies beyond the exemplary OWL-Time, constitutes a way to consistently (and possibly automatically, given more advanced reasoning systems and ontology tools) compare two or more different OWL axiomatizations derived from a first-order axiomatization. The methodology is fairly general. Strong Points: - Using OWL-Time as an exemplar, the paper defines a methodology which uses maximal OWL2-definable subtheories of the mathematical theories used in verifying an ontology, and then showing how these are preserved by synonomy. The authors define SRIQ-Definable theories, Orderings, Bipartite Incidence structures, and use these (via synonomy preservation) to identify the maximal SRIQ-definable subtheories of OWL-TIME from the SRIQ-definable subtheories of a theory. - The paper's contribution can be used and expanded on by others who are interested in comparing (generating) OWL2 ontologies maximally preserving FOL ontology axiomatizations. Weak Points: - Although the presentation of the formal correctness and completeness of the given definitions, theorems, lemmas, and proofs appears sound, there are a couple of potential improvements that could be made: see descriptions provided above. - There is extensive formalism presented in the paper, and therefore clear English descriptions of those formalisms are to be desired, and are not necessarily sufficiently provided. - Some of the external material should be brought into the body of the paper. - There are some English nit: p. 1: "ontologies: is OWL2 ontology" => "ontologies: is the OWL2 ontology" p. 3: "is logically equivalent the translation" => "is logically equivalent to the translation" Footnote 4: "formulæthat" => "formulæ that" p. 5: "the models of subtheory" => "the models of the subtheory" p. 5: Definition 8.3 "R- = R." What is the first symbol, e.g., the complement of R? p. 6: "SRIQ-definable is build" => "SRIQ-definable is to build"

**Review 3 (by anonymous reviewer)**

(RELEVANCE TO ESWC) The topic of this paper is the Time ontology, which is relevant to ESWC. (NOVELTY OF THE PROPOSED SOLUTION) The solution seems novel but more discussion should be provided to justify the novelty. (CORRECTNESS AND COMPLETENESS OF THE PROPOSED SOLUTION) Since many important details are missing (see below), it is difficult to judge the correctness and completeness. (EVALUATION OF THE STATE-OF-THE-ART) Some state-of-the-art is provided but should be extended. (DEMONSTRATION AND DISCUSSION OF THE PROPERTIES OF THE PROPOSED APPROACH) Since many important details are missing (see below), it is difficult to judge the correctness and completeness. (REPRODUCIBILITY AND GENERALITY OF THE EXPERIMENTAL STUDY) Since many important details are missing (see below), it is difficult to reproduce the result. (OVERALL SCORE) Summary of the Paper The paper discusses the maximality of OWL-Time. The reviewer believes it is an important topic to formally charactize the theorectical property of such ontology: whether the ontolgy expressed the corresponding FO aximatization? The authors claim that OWL-Time is in fact not maximal with respect to the firstorder axiomatization. However the main issue is that the paper is not self-contained, thus the reviewer could not follow and appreciate the result of the work. Strong Points (SPs) The topic is important. The motivation is clear. Weak Points (WPs) The paper has several major issue in the writing style: it is not self contained. It just used many terminologies but never introduced them. - For example, the reviewer got stuck at the very first defintion 1: what is "definitional extension"? Moreover, some explanation of the notion "synonymous" should be provided since this is not a common term in the community. - since the paper is about OWL-Time, more details of this ontology should be explained. The authors mentioned several modules "Towltime", "Towltime_mleu", "Tlinear_order", "Tstrong_graphical"... What are these modules? How are they related to the time ontology? - what is "the amalgamation of a model" ? - A minor issue is that the authors do not write "SRIQ" is a consistent format. Please stick to one in which all these letters S,R,I,Q use the same style \mathcal. - The abstract states that "The results show that OWL-Time is in fact not maximal with respect to the first order axiomatization." This seems to be an important conclusion. However, I could not find the corresponding text in the main body of the work. I do believe that this line of research can be potentially important. However, the authors should put more efforts in making the results more accessible. I acknowledged that I have read the rebuttal.

**Review 4 (by Till Mossakowski)**

(RELEVANCE TO ESWC) The paper studies approximation of first-order theories in the description logic SRIQ, which is the logic of OWL2 without nominals. This is an important problem, because many foundational ontologies exists both as FOL theories as well as as OWL2 versions, and it is often not clear whether the OWL2 version is an (optimal) approximation of the FOL version. Indeed, the authors claim to show that the currently existing approximations of the SUMO time ontology in OWL2 is not optimal, which is an interesting result. (NOVELTY OF THE PROPOSED SOLUTION) The results seem to be novel. (CORRECTNESS AND COMPLETENESS OF THE PROPOSED SOLUTION) The paper lacks formal clarity and precision (see detailed comments) and hence should not be accepted in this form. Another major drawback is that the paper is not self-contained: all relevant ontologies are only provided as URLs. Sometimes, even URLs are not clear, e.g. for H^{ordering} or H^{weak_bipartite}. For the URL in footnote 6, I get "The requested URL /ontologies/weak_bipartite.owl was not found on this server." The URL in footnote 3 works, and it is claimed to contain the focus of the present paper. However, it is not clear to me how this URL is related to H^{ordering} or H^{weak_bipartite}, which are the focus of the paper if you look at the theorems. Moreover, it is quite tedious to follow all the imports. Since the paper focusses on theory hierarchies, it would be at least necessary to show an import graph. I have produced one using Hets (http://hets.eu), with hets -g -C http://colore.oor.net=https://raw.githubusercontent.com/gruninger/colore/master/ontologies http://colore.oor.net/owltime_interval/owltime_mleu.clif Still, it did not became clear to me where I find H^{ordering} or H^{weak_bipartite} or the theories in Fig. 2 in this graph. This has not been clarified in the rebuttal. I had to use a different URL that I found when searching the COLORE repository myself. Actually, with hets -g -C http://colore.oor.net=https://raw.githubusercontent.com/gruninger/colore/master/ontologies http://colore.oor.net/bipartite_incidence/strict_graphical.clif I could get a diagram that looks at least similar to Fig. 2. Still, strong_graphical does not occur in my Hets-generated diagram. Nor does weak_loopless. These theories are neither directly nor indirectly imported by strict_graphical. The authors state in the rebuttal that the import closure of the above URL (which I found by myself!) does not suffice. OK, but then please provide some URL where the theories can be obtained, or list some folders of http://colore.oor.net where one should look. Note that even if correct URLs are provided, I think that letting theorems depend on internet material is not acceptable. Another problem is that the referenced first-order ontologies are all written in Common Logic. Now Common Logic has a very peculiar model theory and cannot be equated with standard first-order logic (see also detailed comments). Detailed comments ----------------- p.1 you mention the OWL2 versions of DOLCE. If I recall right, DOLCE's ternary predicates (like temporal parthood) are approximated as (binary) roles in the OWL2 of DOLCE. So this is not an approximation in your sense. p.2 How would you specify the set of intended structures? Is this a finite set? If not, then probably you specify it using a logical theory? So after all, your correctness criterion is given by a logical theory? In the rebuttal, the authors write: "Intended structures of an ontology are specified by classes of structures axiomatized by mathematical theories. A generic ontology is verified by synonymy to the set of mathematical theories." This makes things much clearer. It should be included into the paper. p.3 Def.1 How do you define "definitional extension"? In the rebuttal, the authors write: "We follow the standard definition of definitional extension (see the text "Logic" by Wilfred Hodges, for example)." In this book, definitional extension is not defined. In DOL, T2 is a definitional extension of T1 if every model of T1 has a unique expansion to a model of T2. Do you adopt this notion? If yes, then for example the first-order theories of Boolean algebras and of Boolean rings would be synonymous, which makes a lot of sense. However, this only holds for standard first-order logic. In the case of Common logic, they would be synonymous only if all the symbols are non-discourse names. (With the use of discourse names, the newly added functions in the extension would need to be represented by individuals in the universe of discourse, and this would destroy the above mentioned uniqueness of the expansion.) However, in your COLORE theories, it is not stated that you use non-discourse names. The authors write in their rebuttal: "We avoid the problems of definitional extension in Common Logic by using the Second Edition of ISO 24707. The relations in the signature of theories in H^{bipartite_incidence} are all cl:out discourse (this is specified in colore.oor.net/bipartite_incidence/weak_bipartite.clif, which is imported by all theories in the hierarchy). With this restriction, the models of a Common Logic theory are equivalent to the models of traditional FOL." Then the second edition of ISO 24707 should be referenced. At colore.oor.net/bipartite_incidence/weak_bipartite.clif I could not find "cl:out discourse". p.3, second-last sentence of section 2: "two theories are synonymous iff there is a one-to-one correspondence between the models of the two theories". I can see that the "only if" direction is true. The "if" direction does not hold. Consider the FOL theories Ti axiomatising that the universe consists of exactly i elements, for i=1,2. Then the model class of Ti is the class of sets with i elements. There is an injection from Mod(T1) into Mod(T2): map a set {a} to {(a,0),(a,1)}. There is also an injection from Mod(T2) into Mod(T1): map a set {a,b} to {{a,b}}. By the Schröder–Bernstein theorem, Mod(T1) are Mod(T2) are in bijective correspondence. However, any common extension of T1 and T2 is inconsistent, and hence it cannot be definitional. In the rebuttal, the authors agree to adapt their claim. p.3, Def. 2: what is "the" logic mapping from L1 to L2? Generally, there are many such mappings, so Def. 2 depends on such a mapping as a parameter. It is left unlcear what a logic and a logic mapping is. p.4, Def.6 You should add "Given a hierarchy H of theories in FOL, ..." Moreover, note that for a given FOL theory T, there can be several SRIQ-theories that are language-equivalent (in generally, even infinitely many such theories: consider replacing each axiom C \sqsubseteq D by C \sqcup C \sqsubseteq D etc.). Moreover, the result is a family of SRIQ-theories, hence not a subhierarchy of H. Moreover, the authors should motivate why this definition is better than the use of uniform interpolation. It seems to me that finding a SRIQ-equivalent can be computationally as hard as finding a uniform interpolant (maybe I am wrong, but then I need to be convinced why). But then, why not work with uniform interpolants? The advantage would be that more FOL theories can be approximanted with a uniform interpolant. The authors reply: "The relationship between our techniques and uniform interpolation is interesting, but out of the scope of this paper." I disagree. In my opinion, uniform interpolation should be mentioned, because it is very much related, and there is considerable research. Even if you do not use uniform interpolation, a discussion of related work is needed. p.4, second last paragraph: why should T by a nonconservative extension in general? (I assume that "nonconservative extension" means "extension that is not conservative", and not "an extension that is not necessarily conservative".) In the rebuttal, the authors write: "Since all theories in the same hierarchy have the same signature, every extension is a nonconservative extension." This is an important piece of information that should be added to the paper. p.7 Def. 11 "i=1, j=1" does not make sense - you get just R_{1,1} p.8 Theorem 3: I do not understand the last argument of the proof. Moreover, I would expect that the assumption that T1 is not SRIQ-definable should be used in the proof (otherwise it can be dropped). Apart from that, the theorem is wrong in a subtle way, because OWL2 is not closed in the sense of [A]. Counterexample: T_1={transitive(R), asymmetric(R)}, T_2=\emptyset. T_1 is not SRIQ-definable, but T_2 is not maximally SRIQ-definable. The rebuttal of the authors: "The counterexample does not apply because every theory in a hierarchy is an extension of a unique root theory, and hence $T_2 \neq \emptyset$." The theorem does not mention any hierarchy. But anyway, you can easily modify the counterexample as follows: T_1={transitive(R), asymmetric(R)}, T_2={C \sqsubseteq D}, where C,D are some concepts. p.9 Thm. 5 in the proof, the bijection runs between model classes, not between the theories tehmselves. p.10 l.5 $before$ should be $\mathit{before}$ (otherwise you get strange spacing) p.11 owl, sriq, casl should be upper case. (EVALUATION OF THE STATE-OF-THE-ART) Relevant literature about approximation [A], or uniform interpolation, also called forgetting [B] is not discussed. [A] Marco Console, José Mora, Riccardo Rosati, Valerio Santarelli, Domenico Fabio Savo: Effective Computation of Maximal Sound Approximations of Description Logic Ontologies. International Semantic Web Conference (2) 2014: 164-179 [B] Boris Konev, Dirk Walther, Frank Wolter Forgetting and Uniform Interpolation in Large-Scale Description Logic Terminologies ICJAI 2009 (DEMONSTRATION AND DISCUSSION OF THE PROPERTIES OF THE PROPOSED APPROACH) see "Correctness and Completeness of the Proposed Solution" (REPRODUCIBILITY AND GENERALITY OF THE EXPERIMENTAL STUDY) One could consider this as an experimental study in uniform interpolation. However, it is difficult to reproduce (see the problems with URLs listed unter "Correctness and Completeness of the Proposed Solution") and it is not very general (only a few FOL theories are studied). (OVERALL SCORE) Summary of the Paper Short description of the problem tackled in the paper, main contributions, and results The paper studies approximation of first-order theories in the description logic SRIQ, which is the logic of OWL2 without nominals. This is an important problem, because many foundational ontologies exists both as FOL theories as well as as OWL2 versions, and it is often not clear whether the OWL2 version is an (optimal) approximation of the FOL version. The main result is the characterisation of SRIQ-definable theories in a certain hierarchy of FOL theories. Strong Points (SPs) * the paper studies an interesting problem * the authors have formalised a lot of Common Logic theories * Fig. 2 provides a nice visualisation of the results Weak Points (WPs) * it is not clear which logical theories the authors study, as they are not contained in the paper, but only on the web, and I could not match names for theories and theory hierachies in the paper with the material on the web * there are quite a number of technical errors * relevant literature is not mentioned (approximation, uniform interpolation) *** Questions to the Authors (QAs) 1. what is H^{ordering}? 2. what is H^{weak_bipartite}? 3. what is the correct URL in footnote 6? 4. where do I find the theories shown in Fig. 2? Note that http://colore.oor.net/bipartite_incidence/strict_graphical.clif will not do - it produces a different graph. 5. How do you define "definitional extension"? 6. How do you avoid the problems with definitional extensions in Common logic? 7. what does nonconservative extension mean? 8. How would you specify the set of intended structures of an ontology?

**Metareview by Christoph Lange**

The reviewers agreet that the methodology presented in this paper is useful; however, the following concerns justify rejection: * The formalization is partly hard to follow; some more natural language explanations would help. * Some essential terminology is not clearly defined ("definition extension", "nonconservative extension"). * The paper relies too much on background knowledge that's available externally. * Large parts of the authors' response did not clarify concerns.