Re: SUO: IFF example?
Chris,
At 07:54 AM 5/4/2003 -0500, Chris Menzel wrote:
>On Sat, May 03, 2003 at 11:14:30PM -0700, Adam Pease wrote:
> > >> 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.
>
>I think I misread your original assertion. I *thought* you were saying
>that you had some sort of (meta)proof that proofs under 50 steps have
>some sort of consistency property, e.g., as noted, that no such proof
>contains a statement and its negation. But all you seem to be making is
>the much more modest claim that you have a procedure for terminating
>proofs after, say, 50 steps if an inconsistency hasn't been found and a
>desired conclusion hasn't been reached.
yes, that's right
Adam
> > >> 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.
>
>Ok, that makes sense.
>
>-chris