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