[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: A question from Korea




> Actually, I want to know more profoundly how to prove an AXIOM formated as:

Generally, axioms are facts which are stated without proof that they are
true. They can be a useful tool for writing specifications, but due to
their nature can easily introduce inconsistencies.

> (IF ---- THEN === ELSIF +++ THEN ... ELSE ,,,)
>
> I am using only (prop), (postpone), and (assert), but this seems not to
> be sufficient to me.

A useful command for proving things involving IF expressions, is (smash):

Rule? (help smash)
(SMASH/$ &OPTIONAL (UPDATES? T)) :
    Repeatedly tries BDDSIMP, ASSERT, and LIFT-IF.  If the UPDATES?
option is NIL, update applications are not if-lifted.

Please send more details of exactly what you're trying to do, and
I will try to give more detailed help.

Good luck,
Dave

--
Dave Stringer-Calvert, MEng MACM,  Department of Computer Science,
University of York, Heslington, York, YO1 5DD. [+44|0] 1904 432764