Re: ISSUE: DAML+OIL semantics is too weak

From: "Jos De_Roo" <jos.deroo.jd@belgium.agfa.com>
Subject: Re: ISSUE: DAML+OIL semantics is too weak
Date: Fri, 17 May 2002 21:56:42 +0200

> [...]
> 
> > > 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 have no idea what the distinction you are getting at here is.  There are
several possibilities that I see.

1/ A valid implication, like a -> a v b, but the premise is not true, so
   the conclusion might not be.  An argument that purports to derive a v b
   is incorrect, and any proof system that would sanction it is unsound.

2/ A not-valid implication, like a -> a ^ b, but the premise is true.  An
   argument that purports to derive b is again incorrect, and any proof
   system that would sanction it is unsound.

Neither seems to fit.  Could you please clarify your meaning for me?

> I agree that we have to agree on terminology, so how
> would you call an argument which is based on assumptions
> which are false?

Incorrect, or maybe unsound, but I don't see any difference between this
kind of argument and an argument that uses an incorrect inference.

Maybe you are making a distinction between an argument that uses an invalid
implication and an argument that uses a non-true premise.  However, there
is little difference between the two, as the non-true premise could be the
invalid implication.

> (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 ;-)

Well, if { ?s ?p ?o } follows from some assumptions, most proof systems
will have an infinite number of proof trees for it, so I still don't
understand what you are getting at here.

(It may be that you are trying to say that if ?s has too few known ?p-fillers,
then there is a contradiction, but this does not follow, nor do many of its
variants follow.)

> --
> Jos

peter

Received on Saturday, 18 May 2002 06:29:37 UTC