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:

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

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