Re: completeness

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

peter

Received on Tuesday, 26 February 2008 12:31:59 UTC