From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>

Date: Tue, 26 Feb 2008 10:23:17 -0500 (EST)

Message-Id: <20080226.102317.03381746.pfps@research.bell-labs.com>

To: schneid@fzi.de

Cc: public-owl-wg@w3.org

Date: Tue, 26 Feb 2008 10:23:17 -0500 (EST)

Message-Id: <20080226.102317.03381746.pfps@research.bell-labs.com>

To: schneid@fzi.de

Cc: public-owl-wg@w3.org

From: "Michael Schneider" <schneid@fzi.de> Subject: RE: completeness Date: Mon, 25 Feb 2008 15:35:35 +0100 > Hi Peter! [...] > >Nor does > > > >p r q . > > > >pD* entail > > > >p rdf:type _:e . > >_:e owl:hasValue q . > >_:e owl:onProperty r . > > This entailment is actually explicitly supported by pD*. In this case even > the converse entailment exists (a rare case of "iff"-semantics in pD*). The > respective semantic condition is given by Definition 5.1 in [10]: > > If > (a, b) in E_I(I(hasValue)) > and (a, p) in E_I(I(onProperty)), > then > x in CE_I(a) > if and only if > (x, b) in E_I(p), > > where "E_I(.)" denotes a property extention, and "CE_I(.)" denotes a class > extention. No. The entailment does not go through because there need not be a,b,p such that (a, b) in E_I(I(hasValue)) (a, p) in E_I(I(onProperty)) in models of p r q . > >Nor does > > > >p rdf:type _:s . > >_:s owl:someValuesFrom C . > >_:s owl:onProperty r . > > > >pD* entail > > > >p r _:x . > > Not in pD*, but in "pD*sv", an extention to pD*, which is also specified in > the paper (Definition 6.1). > > However, AFAICS, for pD*sv the paper only provides a completeness result > w.r.t. triple rules. I did not find a complexity bound, neither for > entailment nor for consistency, in contrast to the bounds which exist for > pD*. > So pD*sv might be a little too much as a foundation for OWL-Prime. Probably, as I believe that rule application in pD*sv is non-terminating. Consider, for example, (1) re owl:someValuesFrom re . (2) re owl:onProperty p . (3-0) o1 rdf:type re . Then from (1,2,3-0) rule rdf-svx produces a new b-node _:b1 with (3-1) _:b1 rdf:type re . (4-1) o1 p _:b1 . Then from (1,2,3-1) rule rdf-svx produces a new b-node b2 with (3-2) _:b2 rdf:type re . (4-2) _:b1 p _:b2 . And so on. This inference chain also exists for partial pD*sv closures. [...] > Cheers, > Michael peterReceived on Tuesday, 26 February 2008 15:23:10 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:42:02 UTC
*