- From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
- Date: Thu, 25 Oct 2007 08:29:07 -0400 (EDT)
- To: schneid@fzi.de
- Cc: public-owl-dev@w3.org, gstoil@image.ece.ntua.gr, jjc@hpl.hp.com, phayes@ihmc.us
From: "Michael Schneider" <schneid@fzi.de> Subject: RE: Some basic questions about OWL-Full Date: Thu, 25 Oct 2007 13:23:28 +0200 > 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! ;-)). I don't remember any, but I haven't been exactly looking hard for them. > 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 ^^^ actually simple entailment, not RDF or RDFS entailment > 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. As this lemma is for simple entailment (and thus not only with rdf or rdfs interpretations), it doesn't say anything about whether RDF or RDFS entailment is trivial. > 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? Well RDF interpretations have a non-empty universe, but the Empty Graph Lemma is for simple entailment, which doesn't require interpretations to have any conditons on rdfs:Resource. As simple entailment is, well, *simple*, the proof of the lemma is ... simple. :-) > Cheers, > Michael peter
Received on Thursday, 25 October 2007 12:39:50 UTC