Re: ISSUE: DAML+OIL semantics is too weak

[...]

> > 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.
>
> Are you saying here that your reasoner only uses implications as one-way
> rules?  If so, your reasoner is almost certainly going to be incomplete.

I think so too

> > > > 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.
>
> Do you think that this use of ``UNSOUND'' is standard?  If so, please
point
> me to places in the literature where ``UNSOUND'' is used in this way.

I'm reading Tarski's "Logic, Semantics, meta-mathematics"
[[[
   The consequences of a set of sentences are formed with the
   help of two operations, that of substitution and that of
   detachment (the modus ponens scheme of inference). The
   intuitive meaning of the first operation is clear; we shall
   not, therefore, discuss its character more closely. The
   second operation consists in obtaining the sentence y
   from the sentences x and z=c(x,y)
]]]
so when we made that table, we had better put
P & P->C on top of the soundness collumn
and in our proof arguments we have that P & ...
because the proof tree is actually an RDF graph

--
Jos

Received on Monday, 20 May 2002 07:18:45 UTC