Axiom closures, and the best place for the "Non-Structural Restrictions" chapter

A correction!

I wrote on Tuesday, October 16, 2007 in my mail 

  "Are the acyclicity "nonstructural restrictions" too strict?"
  http://lists.w3.org/Archives/Public/public-owl-dev/2007OctDec/0082.html

>Now, let's regard an ontology which contains the following two axioms:
>
>    (A1) SubObjectPropertyOf(p1 p2)
>    (A2) SubObjectPropertyOf(p2 p1)
>
>Note that these two axioms may either be explicitly stated in 
>the ontology,
>or may be entailed by other axioms, e.g. by an
>'EquivalentObjectProperties(p1 p2)' axiom. For our discussion 
>here this does
>not make a difference, because the nonstructural restrictions 
>deal with any
>axioms occuring in the "axiom closure Ax" of an ontology.

This is wrong! The term "axiom closure" is used several times in the
"Nonstructural Restrictions" chapter

  <http://www.webont.org/owl/1.1/owl_specification.html#7>

but it is not explained in this chapter. So I *wrongly* assumed that this
term means the set of all axioms which can be *semantically* entailed from
the explicitly stated axioms in an ontology. But I now see that the term is
actually defined in chapter 3 of the same document:

  <http://www.webont.org/owl/1.1/owl_specification.html#3>

  "The axiom closure of an ontology O is the smallest set 
  containing all the axioms of O and of all ontologies 
  that O imports."

So the "axiom closure" is the set of axioms which I get when I collect the
axioms of the "base" ontology and all directly and indirectly imported
ontologies. This is completely different from what I thought, and,
specifically, it has nothing to do with the model theoretic semantics of
OWL.

I came to this point when I was wondering if the "Syntax" document is the
right place for the "Non-Structural Restrictions" chapter or not. The reason
for my wondering was, in the first place, my misunderstanding of the term
"axiom closure": If this *were* a semantical term, then the "Syntax"
document would perhaps not be the right document for this chapter. Another
reason for my wondering was that the "Non-Structural Restrictions" chapter
appears to be very different from the rest of the "Syntax" document, both in
style and what it deals with. So this alone deserves a critical
consideration, IMHO.

But now that I know what the term "axiom closure" really means, my
impression is that the "Syntax" document is really the right place for this
chapter. All aspects, which are dealt with in this chapter, are clearly
"non-semantical":

  * The definition of "property expressions" is more or less a repetition of
what is said in chapter 4.2 of the "Syntax" document.

  * The question if a property expression is "composite" or not only depends
on the position where such a property expression occurs in certain
/explicitly/ stated axioms. This question can always be answered by checking
the form of the syntactical expression, by which such an axiom is given.

  * The "object property hierarchy relation" "-->" can always be obtained by
"mechanically" looking if certain axioms /explicitly/ exist. Again, only
syntactical expressions have to be analysed.

  * The reflexive-transitive closure of the "object property hierarchy
relation" "-->" can be algorithmically calculated after "-->" has been
obtained. No more information is needed.

  * The question if a property expression is "simple" or not can be
mechanically decided by simply traversing the above reflexive-transitive
closure "-->*", and check if certain expressions of the form "PE' -->* PE"
exist.

  * The first "non-structural restriction" can be checked for "non-simple"
property expressions by checking all /explicitly/ existing axioms, which are
of the given kind (cardinality restrictions and the like): The check is a
lookup, if the inspected property expression is contained in any of these
axioms or not.

  * The second "non-structural restriction" (acyclicity condition) again is
only about checking the form of certain /explicitly/ existing axioms.

So this all convinces me that the "Nontructural Restrictions" chapter is
well placed in the "Syntax" document. It's all about checking the forms of
certain /explicitly/ existing axioms, and if certain expressions occur in
them or not. This all has nothing to do with semantics, but it has a lot to
do with syntax.

The only thing one could think about is if the title "Nonstructural
Restrictions on Axioms" is the best title possible. But I don't have a
better idea for now. :)

Cheers,
Michael

PS: I have already raised an issue, where I suggest to clarify in the
"Nonstructrural Restrictions" chapter what the term "axiom closure" means,
see

  http://code.google.com/p/owl1-1/issues/detail?id=57

--
Dipl.-Inform. Michael Schneider
FZI Forschungszentrum Informatik Karlsruhe
Abtl. Information Process Engineering (IPE)
Tel  : +49-721-9654-726
Fax  : +49-721-9654-727
Email: Michael.Schneider@fzi.de
Web  : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555

FZI Forschungszentrum Informatik an der Universität Karlsruhe
Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
Tel.: +49-721-9654-0, Fax: +49-721-9654-959
Stiftung des bürgerlichen Rechts
Az: 14-0563.1 Regierungspräsidium Karlsruhe
Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi Studer
Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus

Received on Friday, 19 October 2007 08:12:22 UTC