Re: Some basic questions about OWL-Full

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