RE: completeness

Hello,

See small comment inline.

 
> > >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 .
> 

I guess you could always use some blocking condition to stop the algorithm
and then imply that 

_:b1 p _:b1

...right?

> And so on.   This inference chain also exists for partial pD*sv
> closures.
> 
> [...]
> 
> > Cheers,
> > Michael
> 
> peter

Received on Thursday, 28 February 2008 07:39:57 UTC