RE: [OWLWG-COMMENT] Higher order quantification in OWL-DL with bNodes?

Hi Pat!

Pat Hayes wrote on Saturday, November 10:

>>OWL-DL-1.0 allows me to state that a class :C is the 
>intersection of classes
>>:D1 and :D2. When I have to write such an axiom in RDF 
>syntax, I generally
>>do it by means of Turtle in the following way:
>>
>>   (1) :C a owl:Class .
>>   (2) :D1 a owl:Class .
>>   (3) :D2 a owl:Class .
>>   (4) :C owl:equivalentClass [ a owl:Class ;
>>           owl:intersectionOf ( :D1 :D2 )
>>       ].
>>
>>where (4) is just a convenient Turtle shortcut for writing
>>
>>   (4a) _:X a owl:Class .
>>   (4b) :C owl:equivalentClass _:X .
>>   (4c) _:X owl:intersectionOf ( :D1 :D2 ) .
>>
>>So we actually have a bNode "_:X" in our OWL-DL-1.0 ontology above.
>
>Note however that you could have done a 
>translation with a URIref instead of a bnode 

Yes, this really seems to be an alternative. It took me a while to consider,
whether this is really ok from a semantical point of view (not just a
syntactical trick), but I am now pretty convinced. You might want to check
my considerations:

The bNode says, that there exists /some/ resource, but I do not know which
one. But because it is sure that there /is/ at least one such resource, I
should be allowed to "capture" this unknown resource by introducing some new
(i.e. not used elsewhere) URI ':Y' , which denotes this unknown resource. 

To see this, let's assume that we have a model M for the graph G, which
contains the bNode '_:X'. And let's further assume that G' is the new graph,
in which the bNode '_:X' has been replaced by the URI ':Y'. Then I can use
the model M as a starting point to build all possible interpretations M'_i,
wherein URI ':Y' denotes some resource r_i of the universe. Two different
interpretations M'_i interprete ':Y' by two different resource r_i in the
universe, and for each such resource r_i there is some coresponding
interpretation M'_i. I all other aspects, the interpretations M'_i equal the
original model M. Under these conditions, at least one of all these
interpretations M'_i must be a model for G', because in one of these
interpretations the URI ':Y' will denote a "correct" resource (we know that
there exists one such resource, and I tried them all!). So this means that
for every model for G there is a coresponding model for G', which is
"approximately equivalent" to G. 

The URI ':Y' must of course really be new. If I take an URI which is already
in use elsewhere, then there are already restrictions on this URI given by
class assertions and properties assigned to this URI. Now, when I denote
':Y' by one of the correct resources (one of the resources which exist
acording to the bNode in G), then it might happen that such an
interpretation becomes un-true due to the restrictions existing on the
chosen URI. And in the worst case it may happen that we do not find any
"approximatly equivalent" model for G'.

>(invent some random "skolem" URI for the purpose)

Erm, can you please explain this term to me? I have seen several people
using this term in the WG list recently, but I have never heard about it
before. In Wikipedia I just found some "Skolem Normal Form" (also new to
me), but I do not see whether this has something to do with our discussion
here.

>>Now OWL-DL-1.0 has both a "direct semantics" and an "RDF compatible
>>semantics", and for the DL sublanguage of OWL-1.0 they are 
>intended to be
>>equivalent. This allows me to interprete the above OWL-DL-1.0 
>ontology by
>>using RDF compatible OWL-DL semantics. And because bNodes are 
>interpreted in
>>RDF as /existential variables/, the meaning of axiom (4) is 
>(in natural
>>language):
>>
>>   "There exists some class ?X,
>>   to which class :C is equivalent,
>>   and which is the intersection of the classes :D1 and :D2."  
>>
>>So this statement is actually a quantification about a 
>/class/ variable. But
>>I thought that OWL-DL was a First Order Logic dialect, where 
>all universal
>>and existential quantifications must be asserted about /individual/
>>variables only?
>
>Well, just for clarification, OWL-Full and RDFS 
>are also first-order, 

Ah, I never thought about this for OWL-Full (well, I have just started to
think a bit more deeply about OWL-Full), but after a few considerations
about the existing constructs in OWL (property restrictions, sub class
relationships, etc.) it looks plausible to me that even OWL-Full is a first
order system. Interesting!

>but allow quantification
>over classes. 

Hm, this second part of your statement confuses me. As a test of my
understanding of this situation, shouldn't one better say: 

  "but allow quantification about individuals, 
  which may also be used as classes (i.e. class extensions)
  or properties in the same ontology."

? I do not see any constructs in OWL which really allow me to quantify about
classes (except via bNodes in RDF style ontologies). As I understand it, an
example for a higher order statement would be something like

    FORALL C1 C2: EquivalentClasses(C1 C2) ==> SubClassOf(C1 C2)

This is actually a built-in rule in OWL, but I have no means to explicitly
express such a rule within an OWL-Full ontology. /This/ would really be
quantification about classes, but I do not see that OWL-Full allows me to do
such a kind of higher-order quantification in any form.

>One can quantify over 
>reasonably-sized universes of classes (or indeed 
>anything else) in first-order frameworks. 

This confuses me even more, because I thought that it is the distinguishing
property of first order systems to exclusively allow quantification about
individuals? Well you will certainly know better, perhaps there are
sometimes ways to map class quantifications to equivalent individual
quantifications, so this requirement can be relaxed somewhat, is it this?
But I won't ask you for further explanation of this, because this would
certainly go too far in this thread.

>(What 
>one cannot quantify over is the set of all 
>mathematically definable classes, but nobody 
>wants to do that.)
>
>But your point can still be made, since OWL-DL is 
>a *segregated* first-order language which does 
>not permit individuals and classes to be 
>intermixed, and prohibits quantification over the 
>latter. But see below.
>
>>And in an RDF-mapped OWL-DL-1.0 ontology, I am not allowed
>>to regard such a class variable as an individual variable, 
>because in OWL-DL
>>the OWL universe is strictly separated.
>
>True, but what is the problem? That variable only 
>arises in the RDF translation: it is not a 
>variable in OWL-DL itself. The direct semantic 
>meaning of the intersection statement is clear, 
>and mentions three classes. The RDF meaning of 
>the OWL/RDF is also clear, and also mentions (the 
>same) three classes, but uses two names (the URI 
>":C" and the bnode) to refer to one of them. So? 
>The fact that the RDF uses a name in a way that 
>is syntactically prohibited in the DL says 
>nothing about their semantic equivalence.

I am not sure if I understand this. Does your argumentation go in the
direction that the "intended" axiom

    "Class :C is equivalent to 
    the intersection of the classes :D1 and :D2"

is equivalent to the existentially quantified formulation

    "There exists some class ?X,
    to which class :C is equivalent,
    and which is the intersection of the classes :D1 and :D2."    

? So in this case the existential quantification does no harm, because it is
"fully backed" by the other - equivalent - formulation, which does not
contain any bNode. Is this the idea? This would at least sound reasonable to
me, but perhaps you mean something different.

>Pat

Well, you see, a lot of questions and difficulties in understanding on my
side. It turns out that I am just starting to learn the basics of OWL. :-)

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

Received on Monday, 12 November 2007 08:29:00 UTC