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

>Hi Pat!

Hi Michael

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

Certainly. It comes from the dark ages of 
resolution theorem-proving. Part of the process 
of putting sentences into clausal normal form 
involves eliminating any existential quantifiers 
(since all variables in clauses are universal). 
This is (was?) done by replacing any existential 
occurring inside some universals binding 
variables x1,...xn by a function applied to those 
universal variables, called a Skolem function 
(often written skolem). So for example

(forall (x) (and (P a x)(forall (y)(or (Q x y) (exists (z)(R z))))))

gives the two clauses

(P a x)
(Q x y)(R (f x y))

where f is a skolem function. A skolem constant 
is just a skolem function with no arguments, 
which corresponds to a 'plain' existential 
outside any universals.

If A is a sentence and B is its skolemization, 
then A and B are not FO equivalent, but they have 
the property that (A entails C) iff (B entails C) 
when C does not contain any of the skolem 
functions. So, in particular, one is consistent 
iff the other is. The argument you give above is 
a reprise of the standard proof.

One observation that isn't often made is that if 
we think of skolemization in classical 2nd-order 
logic, and treat the skolem function itself as 
existentially bound, then the two are exactly 
logically equivalent:

(forall (x) (and (P a x)(forall (y)(or (Q x y) (exists (z)(R z))))))
|=2=|
(exists (f) (forall (x) (and (P a x)(forall (y)(or (Q x y) (R (f x y)))))))

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

See above.

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

For translation of all the OWLs into CL, see
http://www.ihmc.us/users/phayes/CL/SW2SCL.html
and
http://philebus.tamu.edu/cmenzel/Papers/AxiomaticSemantics.pdf

>
>>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."
>
>?

Modify that to "which may also BE classes.." and 
its saying the exact same thing I said. Notice Im 
not identifying classes with sets: this 
identification is unique to OWL-DL and is not 
done in RDFS or OWL-Full or Common Logic.

Its important not to think of "individual" as a 
taxonomic classifier. In Tarskian semantics, 
"individual" just means something in the 
universe. A first-order universe can contain 
ANYTHING.

>  I do not see any constructs in OWL which really allow me to quantify about
>classes (except via bNodes in RDF style ontologies).

Well, in OWL-Full, a class may contain classes. 
So suppose A and B are classes containing 
classes, and you say that A is a subclass of B. 
Then you have made a quantified statement about 
classes, in effect. (At any rate, that is what 
you get if you translate this back into 
quantified logic.)

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

owl:EquivalentClasses owl:subPropertyOf owl:SubClassOf .

>  /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, yes, but that is vacuous, since 
"individual" in FO model theory simply means 
"things you are quantifying over". But there is 
nothing in the classical statement of FO model 
theory which prevents these things being of any 
particular kind: they can be sets (class 
extensions), or sets of tuples (relational 
extensions) or anything else.

Exactly what makes a logic or theory 
"first-order" has been investigated, and there is 
a lovely result: its first-order iff it satisfies 
the Compactness and downward Loewenheim-Skolem 
lemmas. Less technically, iff both of:
(1) if S entails A then some finite subset of S entails A
(2) if A is satisfiable then it has a countable model

Modify 'countable' in (2) to 'finite', the finite 
model property, and you get a characterization of 
the decideable fragments of FO logic, including 
DLs.

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

No. Its deeper than this. Take some sentence of ordinary FO logic, say

(forall (x)(if (P x)(Q x))

and ask, what does the quantifier range over? And 
the correct answer is, whatever is in the 
universe of discourse. And then ask, what kind of 
things can be in such a universe? and the correct 
answer is, ANYTHING at all. There are *no* 
restrictions on the nature of things in a FO 
universe of quantification. In particular, one 
classical FO theory might quantify over the 
relations (classes and properties) in another FO 
theory. The classical FO semantic theory allows 
this. What it conventionally does not allow is to 
have these two theories merged into one theory: 
it conventionally forbids using the same name in 
a single theory to denote both individuals and 
relations. But this is an essentially syntactic 
restriction, not a semantic one; and it can be 
removed without doing any essential damage to 
either the syntax, the proof theory or the 
semantics of FO logic. The result is what is now 
called ISO Common Logic.

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

Well, all that is true, but it isn't what I meant 
here. It would do no harm in any case. Your 
observation which started this thread noted that 
one of the OWL-DL semantic conditions, when 
translated into conventional logic (or into RDF, 
but thats not really important) involves what 
appears to be a non-first-order quantification. 
OK, so maybe its really first-order after all: 
but in any case, so what? Even if it were really 
non-FO, that does not itself make OWL-DL non-FO. 
Take conventional FOL and look at a statement of 
the truth conditions for the universal 
quantifier. That involves a second-order 
quantification, but that fact does not in itself 
make FOL second-order. In OWL/RDF there are two 
distinct languages involved: RDF and its 
semantics, and OWL and its semantics. The extra 
semantic constraints which make OWL/RDF 
equivalent to 'abstract' OWL are conditions which 
when added to the RDF semantics, produce 
truth-conditions which are equivalent (on the 
OWL-DL-syntactically legal subcase) to the 
abstract semantics. Nothing in that says that 
these extra conditions have to be stated in any 
particular (FO or SO) 'style' in order for the 
language being defined to be of any particular 
class.

Pat

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


-- 
---------------------------------------------------------------------
IHMC		(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32502			(850)291 0667    cell
phayesAT-SIGNihmc.us       http://www.ihmc.us/users/phayes

Received on Monday, 12 November 2007 15:46:18 UTC