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

Date: Tue, 26 Feb 2008 07:25:07 -0500 (EST)

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

To: schneid@fzi.de

Cc: public-owl-wg@w3.org

Date: Tue, 26 Feb 2008 07:25:07 -0500 (EST)

Message-Id: <20080226.072507.102777939.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: Fri, 22 Feb 2008 16:56:20 +0100 > Hi Peter > > Peter F. Patel-Schneider wrote: > > >> Alan, > > > >[...] > > > >> In terms of "completeness," I think pD* rules are complete > >> (correct me if I am wrong on this please). > > > >Not quite. The pD* rules need an auxiliary test for contradictions. > >They could probably be made refutation complete. > > Hm, I'm not sure whether I understand this. > There are of course at least two notions of "completeness" around > here. One is the completeness of the triple rules w.r.t. the > model-theoretic semantic conditions. The other one is regarding how > much of this rule corpus is actually implemented. I will distinguish > between these notions by "ruleset completeness" vs. "implementation > completeness". But I do not see how any of these two notions matches > the "contradiction test" case you mention. > For the "ruleset completeness" case, to my understanding this means the > following: > > "Given two RDF graphs G1 and G2. > Whenever G1 pD*-entails G2 by means of the model-theoretic semantic > conditions, then there exists a finite sequence of rule applications > which lead from G1 to G2." This is *not* correct for the rules listed for pD*. > For the "implementation completeness" case, I think this means for a > specific reasoner: > > "Given two RDF graphs G1 and G2: > If there is a finite sequence of rule applications which lead from G1 > to G2, then the reasoner says 'yes'." > > I do not see where the contradictions come into play here. I can, of > course, > ask for a special graph G2* which encodes some contradiction in triple > form, > and ask if another graph G1* entails G2*, e.g: > > G2* := { > x owl:sameAs y > x owl:differentFrom y > } > > Do you mean that for pD* there are two such graphs G1* and G2*, where > G1* entails G2* model-theoretically, but there is no respective > rule-sequence? Yes. Consider a G1 that is inconsistent. > Or that for each reasoner there exist such two counter-example graphs on > which the reasoner fails to recognize the entailment? I say nothing about particular reasoners. > Btw: What is meant by the term "refutation complete"? Refutation complete means that the rules produce a special "inconsistent" marker whenever the input is inconsistent, but that they may not produce all consequences otherwise. > Cheers, > Michael peterReceived on Tuesday, 26 February 2008 12:31:59 GMT

*
This archive was generated by hypermail 2.2.0+W3C-0.50
: Tuesday, 26 February 2008 12:32:00 GMT
*