Re: completeness

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

peter

Received on Tuesday, 26 February 2008 15:23:10 UTC