Paper 75 (Research track)

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.


Share on

Leave a Reply

Your email address will not be published. Required fields are marked *