Theorem proving isn't
the same as simplification. If you are interested in
whether an expression E is always true, I guess you can
try to prove E=true.
I do not know how access to facts would be incorporated.
Compiling some program isn't the same as understanding it :)
RJF
C Y wrote:
>--- Richard Fateman <fateman@cs.berkeley.edu> wrote:
>
>
>>I just compiled and loaded NQTHM into a Maxima running
>>in Allegro Common Lisp. From looking at the documentation,
>>it seems NQTHM runs in CLISP and GCL and CMU lisp already.
>>
>>
>
>Wow. That's certainly a good start. Are you using the 1992 version?
>
yes.
There is a patch to SLOOP needed. (Actually, the patch is to not load
SLOOP at all).