Re: a problem with comprehensive entailments

Jos,

Is there a way that you can place a finite boundary on the number of times
this back and forth will occur, that is, is there a way, using comprehensive
entailments, that you will be absolutely certain that the entailments are
actually comprehensive? For example, suppose we decide to go with this
approach, and then just after CR, for example, someone demonstrates yet
another example of a paradox for which no easy rule can be developed. What
then?

Jonathan



>
> > > I believe we have three live proposals:
> > >
> > > - comprehensive entailments: Jeremy
> >
> > Unfortunately, this proposal is fatally flawed.
> >
> > In the empty KB, we can apply the kitchen sink comprehension rule
> >
> > (forall (?v)
> > (=> (and (Type ?p Property)
> >          (Type ?card NonNegativeInteger)
> >          (Type ?min NonNegativeInteger)
> >          (Type ?max NonNegativeInteger)
> >          (Type ?c1 rdfs:Class)
> >          (Type ?c2 rdfs:Class))
> >      (exists (?r) (and (Type ?r Restriction)
> >                       (PropertyValue onProperty ?r ?p)
> >                       (PropertyValue minCardinality ?r ?min)
> >                       (PropertyValue maxCardinality ?r ?max)
> >                       (PropertyValue cardinality ?r ?card)
> >                       (PropertyValue hasClass ?r ?c1)
> >                       (PropertyValue toClass ?r ?c2)  ) ) ) )
> >
> > with ?p as rdf:type
> >      ?card as 0
> >      ?min as 0
> >      ?max as 0
> >      ?c1 as rdfs:Class
> >      ?c2 as rdfs:Resource
> >      ?v as rdf:type (?v is not used in the rule)
> >
> > to obtain the following restriction (written in n-triples notation)
> >
> >    _:r rdf:type owl:Restriction .
> >    _:r owl:onProperty rdf:type .
> >    _:r owl:minCardinality 0 .
> >    _:r owl:maxCardinality 0 .
> >    _:r owl:cardinality 0 .
> >    _:r owl:hasClass rdfs:Class .
> >    _:r owl:toClass rdfs:Resource .
> >
> > Now consider whether rdfs:Class is a member of this restriction.
> >
> > Because _:r has both owl:onProperty and owl:toClass, an object belongs
to
> it
> > exactly when all its rdf:type fillers belong to rdfs:Resource.  But this
> is
> > true of all objects in all interpretations.  Therefore rdfs:Class
belongs
> > to _:r.
> >
> > Because _:r has both owl:onProperty and owl:maxCardinality, an object
> > belongs to it exactly when it has at most 0 rdf:type fillers.  But this
> is
> > not true of rdfs:Class, because rdfs:Class has rdfs:Class as an
rdf:type.
> > Therefore rdfs:Class does not belong to _:r.
> >
> > Therefore an empty knowledge base implies that some object both belongs
> and
> > does not belong to some class.
>
> OK
> with the following pair of ``entailment'' rules
>
>   { :rule9r1 .
>     ?s a ?C }
>     log:implies
>       { ?s a [ a owl:Restriction;
>                owl:onProperty rdf:type;
>                owl:toClass ?C ] } .
>
>   { :rule9r2 .
>     ?s a ?C }
>     log:implies
>       { ?s a [ owl:complementOf [ a owl:Restriction;
>                                   owl:onProperty rdf:type;
>                                   owl:maxCardinality "0";
>                                   owl:hasClass ?C ] ] } .
>
> we were able to entail
>
>   rdfs:Class a [ a owl:Restriction;
>                  owl:onProperty rdf:type;
>                  owl:toClass rdfs:Resource ] .
>
>   rdfs:Class a [ owl:complementOf [ a owl:Restriction;
>                                     owl:onProperty rdf:type;
>                                     owl:maxCardinality "0";
>                                     owl:hasClass rdfs:Class ] ] .
>
> and we have kept some statements in appropriate N3 contexts
>
> --
> Jos
>
>

Received on Sunday, 5 May 2002 20:40:04 UTC