RE: Some basic questions about OWL-Full

Hi Peter (and Pat and Jeremy)!

Peter F. Patel-Schneider wrote:

>Well you could certainly ask the same question about RDF, or RDFS.
>
>Indeed, some care has to be taken with D-entailment when XML Schema
>datatypes are considered, as the XML Schema datatype document, read
>normally, is internally inconsistent. 

Except from this datatype problem, I am curious to learn whether there is
any consistency proof for RDF(S) semantics? This would be interesting to
see, because it would show me, as an example, what one has to do to proof
the consistency of an ontology language like OWL-Full (no, of course, I am
*not* planning to try this, it's just to satisfy my curiosity! ;-)).

>From a quick look I can see myself that there are several proven lemmas in
the "RDF Semantics" document at

    http://www.w3.org/TR/rdf-mt/#prf

And the first of these lemmas even directly deals with the "empty graph"
question for RDF (analog to Jeremy's "empty OWL-Full ontology" question in
one of his previous mails):

    "Empty Graph Lemma.
    The empty set of triples is entailed by any graph, 
    and does not entail any graph except itself."

So at least in RDF(S?) the "trivial empty graph" problem does not seem to
exist, because the second part of this lemma tells that the empty graph does
not entail any further RDF statements, and so especially no contradictory
statements. But I am reluctant to dig deeper into this appendix to look
whether there is a complete consistency proof included, or whether such a
proof results from the given lemmas as an easy corollary (this is the first
time I look at this appendix, and so I am not familiar with it).

Any comments?

BTW (looking a second time at the "Empty Graph Lemma" above): I wonder why
the empty RDF graph does not entail the triple "_:x rdf:type rdfs:Resource",
i.e. the existentially quantified statement: "There exists some resource".
Haven't we previously discussed that RDF semantics demands a non-empty
universe?

Cheers,
Michael

>* The value space of decimal is the set of numbers that can be
>  obtained by multiplying an integer by a non-positive power 
>of ten, i.e.,
>  expressible as i x 10^-n where i and n are integers and n >= 0
>
>So, the integer 2 is in the value space of xsd:decimal.
>
>* The basic value space of float consists of the values m x 
>2^e, where m
>  is an integer whose absolute value is less than 2^24, and e is an
>  integer between -149 and 104, inclusive. 
>
>So, the integer 2 is in the value space of xsd:float.
>
>* The value spaces of all primitve datatypes are disjoint.
>
>Contradiction.
>
>This contradiction is "resolved" by making the overall value space
>contain the disjoint union of the value spaces of the primitive
>datatypes, and thus "2"^^xsd:decimal is not equal to "2"^^xsd:float.
>
>peter
>
>
>From: "Giorgos Stoilos" <gstoil@image.ece.ntua.gr>
>Subject: RE: Some basic questions about OWL-Full
>Date: Thu, 25 Oct 2007 10:15:54 +0300
>
>> Hi all,
>> 
>> Does this question/discussion apply also to RDF or only to 
>OWL Full. If so
>> why is there a difference?
>> 
>> Best,
>> Giorgos
>> 
>> > -----Original Message-----
>> > From: public-owl-dev-request@w3.org 
>[mailto:public-owl-dev-request@w3.org]
>> > On Behalf Of Pat Hayes
>> > Sent: Wednesday, October 24, 2007 1:26 AM
>> > To: Michael Schneider
>> > Cc: public-owl-dev@w3.org; Peter F. Patel-Schneider; jjc@hpl.hp.com
>> > Subject: RE: Some basic questions about OWL-Full
>> > 
>> > 
>> > >Pat Hayes wrote:
>> > >
>> > >>>From: Pat Hayes <phayes@ihmc.us>
>> > >>>Subject: Re: Some basic questions about OWL-Full
>> > >>>Date: Tue, 23 Oct 2007 08:58:28 -0500
>> > >>>
>> > >>>>
>> > >>>>   >Peter F. Patel-Schneider wrote:
>> > >>>>   >>
>> > >>>>   >>For homework:  Is EquivalentProperties(owl:sameAs
>> > >>owl:differentFrom)
>> > >>>>   >> 	 	       itself inconsisten?
>> > >>>>   >>
>> > >>>>   >
>> > >>>>   >I'm afraid I'm several years' late on my (easier) 
>homework of:
>> > >>>>   >    Is (*empty*) itself inconsistent?
>> > >>>>
>> > >>>>   Yes, in RDF (and conventional FOL). This is the
>> > >>>>   only assumption of Tarskian semantic theory, that
>> > >>>>   there is something in the universe. One can build
>> > >>>>   a 'free' logic which allows an empty universe,
>> > >>>>   but then its proof theory can't have the usual
>> > >>>>   rules of instantiation and generalization, which
>> > >>>>   allow the inferences
>> > >>>>
>> > >>>>   (forall (x) (foo x))  |==   (foo A) for some
>> > >>>>   'new' name A |==  (exists (x)(foo x))
>> > >>>>
>> > >>>>   Pat
>> > >>>
>> > >>>I think Jeremy meant an empty KB, i.e., whether OWL 
>Full is trivial or
>> > >>>not.
>> > >>
>> > >>Ah, I see. Sorry. Yes, that question amounts to
>> > >>whether the OWL semantic conditions are
>> > >>internally consistent when transcribed into
>> > >>common logic (or FOL using the holds/app style).
>> > >>Good question!
>> > >
>> > >Hm, seems to me that I did not understand neither Jeremy, 
>nor Peter, nor
>> > >you. :) What is meant by "whether OWL Full is trivial or not"?
>> > 
>> > "Trivial" in this context means that there would
>> > be no OWL-Full interpretations which satisfy
>> > anything, so everything would be OWL-Full
>> > unsatisfiable. Put another way, the OWL-Full
>> > semantic conditions would be internally
>> > contradictory.
>> > 
>> > >  Is this the
>> > >question about whether empty OWL-Full ontologies are 
>inconsistent or not?
>> > 
>> > That is another way to put it, yes.
>> > 
>> > >I.e. whether an empty OWL-Full ontology entails 
>contradictory statements?
>> > 
>> > And that is another, yes.
>> > 
>> > >But if I have some arbitrary non-empty ontology O := 
>{A1,...,An}, then O
>> > >contains the empty ontology as a sub-ontology. So I would 
>assume that
>> > every
>> > >statement which is entailed by the empty OWL-Full 
>ontology will also be
>> > >entailed by O itself. And if the empty OWL-Full ontology 
>would entail
>> > >contradictory statements, then /every/ OWL-Full ontology 
>would entail
>> > >contradictory statements, and then OWL-Full semantics 
>would be totaly
>> > >broken!
>> > 
>> > Quite. Which is what Peter meant by "trivial". I
>> > am confident that this is not the case, but even
>> > if it were I would say they would indeed be
>> > broken, but because in that case the OWL semantic
>> > conditions were themselves broken. And not
>> > necessarily totally, since the next task would be
>> > to see how to weaken them so that they weren't
>> > broken. IMO they are too strong in some ways in
>> > any case, e.g. the intensional view of classes
>> > seems better than the extensional one, c.f.
>> > terHorst's version of OWL.
>> > 
>> > >Is it this what you (Pat) mean by "whether the OWL semantic
>> > >conditions are internally consistent..."?
>> > 
>> > Yes.
>> > 
>> > Pat
>> > 
>> > >
>> > >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
>> > 
>> > 
>> > --
>> > 
>---------------------------------------------------------------------
>> > 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
>> > 
>> 
>> 
>

--
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 Thursday, 25 October 2007 11:23:50 UTC