RE: ACTION-93 / ISSUE-63: Initiated work on OWL-1.1-Full semantics

Hi Peter!

Peter F. Patel-Schneider wrote on Wednesday, March 26, 2008:

>> >2/ I do not believe that a comprehension principle is needed for
>> >   owl11:disjointUnionOf (so long as there is a 
>comprehension principle
>> >   for lists of descriptions) and the syntax requires that the
>> >   disjointUnion be a named class.
>> 
>> I don't understand your last remark about the requirement of 
>a named class.
>
>If a named class is required (and it currently is)
>
>disjointUnion := 'DisjointUnion' '(' { annotation } 
>owlClassURI description description { description } ')'
>
>then there is no need to ever require the existence of a node on the
>"left hand side" of an owl:disjointUnionOf because the only nodes that
>are needed there to make entailment work out are named classes.  

I don't see a way to perform such a restriction to only /named/ classes in OWL-Full. 

This is, of course, possible in OWL-DL, which demands that an ontology has to be syntactically valid to its Abstract/Functional syntax. This syntax can then restrict the use of a node within a certain language construct to be only an URI. And the OWL-DL semantics are then only specified for such a syntactically valid expression. 

But how can I specify such a constraint in OWL-Full, for which /every/ RDF graph is a syntactically valid input and gets interpreted by OWL-Full semantics? 

[...]

>> (A) How do you think about my approach to introduce the 
>"missing" axiomatic
>> triples? Was is intended to not include them, and if so, for 
>what reason? Or
>> has it just been forgotton?
>
>It was intended not to include them.  It's not as if there are any real
>problems if these are not included, and, again, putting them in just
>increases the chance of some unintended consequence.

In principle, I share this stance, because I have not yet seen a real advantage for having axiomatic triples in RDF(S). But in this case, I would have expected to see /no additional/ axiomatic triples at all in OWL-Full. However, OWL-Full has lots of them!

* Everything listed in the section "OWL built-in syntactic classes and properties" is in fact an axiomatic triple, even if it is not called so explicitly. For example, saying "I(owl:FunctionalProperty) is in C_I" (btw: it should be "S_I(owl:FunctionalProperty)", right?) corresponds to the axiomatic triple

  owl:FunctionalProperty rdf:type rdfs:Class

There are 33(!) axiomatic triples of this kind alone in this single section. And there are several more in the "parts of the OWL universe" table. For example, the third entry about E := owl:Restriction contains two of them:

  owl:Restriction rdf:type rdfs:Class        # "S_I(E) in C_I"
  owl:Restriction rdfs:subClassOf owl:Class  # "IOR subset IOC"

There are no premises of the form: "if a certain triple containing these entities exist in the graph, then...", and so these assertions are true for every graph, in particular they are entailed by the /empty/ graph.

My idea was to just add the /missing/ axiomatic triples. I did not see a clear criterion for why those which exist are in, and why those which do not exist are not in. The selection looks all a bit random to me. I wanted to have a somewhat more systematic approach, or at least follow existing precedence, and so I thought to follow the lead of RDFS.

Btw: I believe that there are people in the RDF-semantics world who actually assume that the missing axiomatic triples are in OWL-Full. For example, I can see that the domain and range axiomatic triples for the owl:onProperty property is listed in the pD* paper. But since it is not given in the OWL-Full spec, this means that pD* is /not/ a semantical sublanguage of OWL-Full. I suspect that this will come to a surprise to the author of pD*. 

>> (B) Why are there only "ONLY-IF" semantic conditions for 
>restrictions? The
>> introduction of sec. 5.2 in the AS&S says:
>> 
>>   "The only-if semantic conditions for the [restrictions] are needed 
>>   to prevent semantic paradoxes and other problems with the 
>semantics."
>
>> Can you please elaborate on this?
>
>Suppose all the conditions are IFF, including
>
>\forall y in IOC \forall x in IOR \forall p in IOOPuIODP
>( <x,y> in EXTI(SI(owl:allValuesFrom)) and
>  <x,p> in EXTI(SI(owl:onProperty)) )
>iff
>CEXTI(x) = { u in IOT | <u,v> in EXTI(p) implies v in CEXTI(y) }
>
>\forall y in IOC \forall x in IOR \forall p in IOOPuIODP
>( <x,y> in EXTI(SI(owl:someValuesFrom)) and
>  <x,p> in EXTI(SI(owl:onProperty)) )
>iff
>CEXTI(x) = { u in IOT | E <u,v> in EXTI(p) such that v in CEXTI(y) }
>
>Then consider an interpretation with 
>
>p1/ EXTI(SI(p)) = { < SI(i),SI(v) > }
>
>p2/ EXTI(SI(q))(SI(i)) = { }
>p3/ EXTI(SI(q))(x) = { x } for x not SI(i) 
>
>p4/ CEXTI(SI(c)) = { SI(i) }
>
>and some other less interesting stuff
>
>Then we get 
>
>c1/ CEXTI(SI(c)) = { u in IOT | E <u,v> in EXTI(SI(p)) such 
>that v in CEXTI(SI(owl:Thing)) }
>
>c2/ CEXTI(SI(c)) = { u in IOT | <u,v> in EXTI(SI(q)) implies v 
>in CEXTI(SI(owl:Nothing)) }
>
>so from c1 
>
>c3/ <SI(c),SI(owl:Thing)> in EXTI(SI(owl:someValuesFrom))
>c4/ <SI(c),SI(p)> in EXTI(SI(owl:onProperty))
>
>and also
>
>c5/ <SI(c),SI(owl:Nothing)> in EXTI(SI(owl:allValuesFrom))
>c6/ <SI(c),SI(q)> in EXTI(SI(owl:onProperty))
>
>but then from c4 and c5 we get 
>
>c7/ CEXTI(SI(c)) = { u in IOT | <u,v> in EXTI(SI(p)) implies v 
>in CEXTI(SI(owl:Nothing)) }
>
>and then (with p4)
>
>c8/ <SI(i),v> in EXTI(SI(p)) implies v in CEXTI(SI(owl:Nothing))
>
>which contradicts p1
>
>and from c3 and c6 we get
>
>c9/ CEXTI(SI(c)) = { u in IOT | E <u,v> in EXTI(SI(q)) such 
>that v in CEXTI(SI(owl:Thing)) }
>
>and then (with p4)
>
>c10/ Ev <SI(i),v> in EXTI(SI(q))
>
>which contradicts p2.

Many thanks, I now understand the principle problem.

>Which I suppose is not a complete collapse of the semantics, but is
>certainly not what you want.

Would it surprise you to hear that the collapse (i.e. the unsatisfiability of OWL-Full) would happen under IFF semantics for restrictions? :)

Cheers,
Michael

--
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