RE: completeness

Hi Michael,

> -----Original Message-----
> From: Michael Schneider [mailto:schneid@fzi.de]
> Sent: Friday, February 29, 2008 11:23 AM
> To: Giorgos Stoilos; Peter F. Patel-Schneider
> Cc: public-owl-wg@w3.org
> Subject: RE: completeness
> 
> Hi Giorgos and Peter!
> 
> Giorgos Stoilos answered to Peter F. Patel-Schneider:
> 
> >> > >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?
> 
> Hm, I certainly do not understand what you mean by a "blocking condition"
> here. At least, alone from the axioms (1)-(3-0), I cannot see anything
> which allows me to assume that there exists some instance of class re
> which has p-relationship to itself, i.e. that a "loop" triple '_:b1 p
> _:b1' can be entailed. It is only stated that:
> 

Blocking is a technique/condition used in some reasoning algorithms that are
known to have termination problems in order to stop the execution at some
point. 

Consider the above example: Someone comes and tells you "OK, your reasoner
stopped and told that the knowledge base is satisfiable. But can you
actually construct a model from what the algorithm has created, i.e. is the
knowledge base indeed satisfiable". Then you start thinking...ok, _:b1 is in
class re, so it "must" have a p-relationship to some entity y which also
*must* live in class re, otherwise what you are going to create would not be
correct. But your algorithm hasn't created that entity...what to do? Just
use _:b1 which you already know that it is in re and create a loop.

Obviously this does not mean that your knowledge entails '_:b1 p _:b1'. But
on the other hand this is a possible model of your knowledge that you can
create in order to prove that such a model actually exists and the reasoner
does not give false answers (i.e. is sound).

>   "If entity x is in class re,
>   then it has a p-relationship to some entity y
>   which also lives in class re."
> 
> y may or may not coincide with x; in general one cannot expect this to be
> the case.
> 
> In fact, if my universe is the set of integers, and my property p denotes
> the 'smallerThan' relation, then I wouldn't want this someValue
> restriction to allow such a loop triple at all. I can even define class re
> to be a someValue restriction on property p := owl:differentFrom, in which
> case such loops would be formally disallowed to exist.
> 

Indeed you could very simply say that p is an inverseFunctional property. So
then again a loop would not be possible since 

_:b1 p _:b1 . implies _:b1 p^- _:b1 . and 
  o1 p _:b1 . implies _:b1 p^- o1 . 

where p^- is the inverse of p and you are again in trouble ;)


OK...so how to create a model now? This could again be done. Just create an
infinite model with no loops: _:bi p _:bi+1 ., _:bi rdf:type re .  i a
positive integer.

Remark: This is not to suggest that the algorithm of pD*sv could be tuned in
order to always terminate, but just for the record blocking might be used to
remedy the example given above.

Hope that was clear enough.

Greetings,
G. Stoilos

> So, at the moment, I do not see any method to stop the inference chain.
> But perhaps I misunderstood you completely?
> 
> >> And so on.   This inference chain also exists for partial pD*sv
> >> closures.
> >>
> >> [...]
> >>
> >> > Cheers,
> >> > Michael
> >>
> >> peter
> 
> @Peter: This was an interesting and pretty convincing example, thanks!
> 
> Cheers,
> Michael
> 
> --
> Dipl.-Inform. Michael Schneider
> FZI Forschungszentrum Informatik Karlsruhe
> Abtl. Information Process Engineering (IPE)
> Tel  : +49-721-9654-726
> Fax  : +49-721-9654-727
> Email: Michael.Schneider@fzi.de
> Web  : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555
> 
> FZI Forschungszentrum Informatik an der Universität Karlsruhe
> Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
> Tel.: +49-721-9654-0, Fax: +49-721-9654-959
> Stiftung des bürgerlichen Rechts
> Az: 14-0563.1 Regierungspräsidium Karlsruhe
> Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi Studer
> Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus

Received on Friday, 29 February 2008 14:55:19 UTC