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 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?

From the table

    Premise     ->     Conclusion
----------------------------------------------------
(1) False     True     False       VALID     UNSOUND
(2) False     True     True        VALID     UNSOUND
(3) True      False    False       INVALID   UNSOUND
(4) True      True     True        VALID     SOUND

and having that
  :R a [ owl:complementOf :R ]
is the same proposition as
  not(:R a :R)
we have the case
  not(p) -> p
so only (2) or (3) are to be considered
but both are UNSOUND

So we aim at (4)'s but in our backing up
with running cose (just FYI) we don't work
with the not()'s but instead try to prove
that the the premise is true and have the
other rule as candidate but then we are
no longer on an a so called "Euler path"
and don't derive from vicious circles.

> > 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.

I agree, that would make no difference.
It's just that we call such a non-true premise implication
(and an INVALID implication) an UNSOUND proof argument.

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

OK, I now see some problems, thanks.
The point was to count the number of ?p instance pairs
so I have to make sure to count the proof tree conclusions
that are different (the cardinality of the proof tree set).
I think about that infinity...

--
Jos

Received on Saturday, 18 May 2002 08:47:44 UTC