Re: ISSUE: DAML+OIL semantics is too weak

[...]

> > 1) there is one thing I would like to reiterate
> > suppose we have a paradoxical pair such as e.g.
> >
> > I1 = { ?x a :R } log:implies { ?x a [ owl:complementOf ?x ] } .
> > I2 = { ?x a [ owl:complementOf ?x ] } log:implies { ?x a :R } .
>
> This says that a resource belongs to :R iff it does not belong to itself.
>
> So, does :R belong to :R, and what can be gained from this?
> Well, if :R belongs to :R then :R does not belong to :R, which cannot be,
> so no model of the above has :R belonging to :R.
> However, if :R does not belong to itself then :R belongs to :R, which
> cannot be, so no model of the above has :R not belonging to :R.
> Therefore the two implications above have no models.
>
> > then deriving a contradiction from that is indeed a
> > VALID inference but it is not a SOUND inference and
>
> The above reasoning is SOUND.
> SOUND reasoning means that the derived formulae semantically follow from
> the assumptions, i.e., that if you can derive X from A1, ..., An,
> then A1, ..., An entails X.  But I1, I2 has no models, so I1, I2 entails
X
> for any X, so deriving any X from I1, I2 is indeed SOUND reasoning.

All we wanted to say is that
  { :R a [ owl:complementOf :R ] } log:implies { :R a :R } .
or simplified
  :R a :R .

could be argued, but ***according to that rule*** the
premise is FALSE and we (in our oldfashioned mode)
call that an UNSOUND argument (although it is VALID)
and we avoid such derivations.
I agree that we have to agree on terminology, so how
would you call an argument which is based on assumptions
which are false?
(and which is something we should avoid I think,
otherwise "if I see 2 suns, my aunt is a car"
and also in case of true premises we can simplify a
proof argument to its conclusion or T -> C as C)


> > 2) yes, more desirable consequences should follow
> > from more implications, but also there should
> > be more rules for deriving inconsistencies
> > such as e.g.
> >
> > { :rule16r1 .
> >   ?s ?p ?o .
> >   ?s a [ a owl:Restriction;
> >          owl:onProperty ?p;
> >          owl:minCardinality ?min;
> >          owl:maxCardinality ?max;
> >          owl:toClass ?C ] .
> >   { ?s ?p ?o . ?o a ?C } math:entailCount ?n .
> >   ?n math:lessThan ?min
> > }
> > log:implies
> > { ?s :inconsistentWith owl:Restriction } .
> >
> > where math:entailCount is just something to count
> > how many times we can entail its subject graph
> > from what was given
>
> The above DAML+OIL restriction says that the set of resources that have
> atleast ?min fillers for ?p that belong to ?C is the same as the set of
> resources that have atmost ?max fillers for ?p that belong to ?C.  From
> this weird restriction lots of unusual consequences result.  I think that
> it would be much better if you revised your example to eliminate the
> weirdness.  I can't determine what is supposed to be happening here
otherwise.

Oops, that second line
  ?s ?p ?o
is there too much, as are other things, so something like

{ :rule16r1 .
  ?s a [ a owl:Restriction; owl:onProperty ?p; owl:minCardinality ?min ] .
  { ?s ?p ?o } math:proofCount ?n .
  ?n math:lessThan ?min }
log:implies
{ ?s :inconsistentWith owl:Restriction } .

(but I have to check with running code and reread DAML+OIL ASAP)


> Also, I have no idea what
>
> > how many times we can entail its subject graph
>
> means.
>
> Entailment just is, it is not a process that can be performed a number of
> times.

Well again "proof argument" wise, this is in the sense of
  "how many proof trees can we find for { ?s ?p ?o }"
and that number should be less than ?min
Naming things such as math:proofCount
seems to be the more difficult job ;-)

--
Jos

Received on Friday, 17 May 2002 15:57:20 UTC