Re: SUO: IFF example?
Hi Chris,
At 05:15 PM 5/3/2003 -0500, Chris Menzel wrote:
>On Fri, May 02, 2003 at 02:00:27PM -0700, Adam Pease wrote:
> > >I believe that SUMO and OpenCyc are in fact not logically consistent
> > >overall, but there may be portions that are consistent, or can be
> > >made so with small modifications.
> >
> > Do you mean that they are not mutually consistent, or that they are
> > not internally consistent? I suspect the former is true, to some
> > degree,
>
>Truths about consistency don't really come in degrees, Adam. Your
>theory is consistent or it isn't.
You're right. I was speaking too loosely.
> > we have done proofs for consistency within specified time boundaries.
>
>What is consistency within a specified time boundary? Would this be the
>idea: a set A of sentences is consistent within a boundary of 50 if no
>proof under 50 steps contains both a formula and its negation. Is that
>right? If so, how would one go about proving such a thing?
Automated proof is a search, so one can simply terminate the search after a
certain amount of time, if results haven't already been returned.
> > We found and removed inconsistencies found in up to 50-step proofs.
>
>I do not understand this result at all. If you find an inconsistency in
>a proof, there's no "removing" it. You just stop asserting its
>premises (and you hopefully find which premises are false).
Yes, that's what I meant by removing the inconsistency. When we've
discovered an inconsistency, that has alerted us to an axiom that was
incorrect, so we change the axiom and that removes the
inconsistency. Since such a change could introduce a new inconsistency,
it's necessary then to rerun the consistency check.
> > We can run for days now without finding anything, so we have some
> > degree of confidence that SUMO is internally consistent.
>
>I think that is a wholly unwarranted conclusion -- at most it seems to
>provide some justification for the (still perhaps significant)
>conclusion that many useful subsets of SUMO are consistent.
Ok, that sounds like a more exact way of expressing it.
Adam
>-chris