--- 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?
> I don't know how the systems compare in usefulness.
> NQTHM seems to have some kind of fortran verifier example
> and some proofs of lisp programs.
Just so there is no confusion (or rather to highlight mine), the hope
would be to use the logic of this system as a replacement for the
current rules for things like FOR, AND, OR, >, <, >=, <=, etc? It may
be lack of sleep but I'm curious as to how the feature set of NQTHM
would map into Maxima. Would Maxima provide the math "facts" and
NQTHM's algorithms supply the logic to manipulate them? I'm sure
that's not the right question but maybe someone can see what I mean.
Stavros clearly pointed out weaknesses in our current boolean and
relational abilities - I'm curious how well the logic translates
between the NQTHM environment and the Maxima environment, and whether
it fits the bill.
CY
__________________________________
Do you Yahoo!?
Yahoo! Hotjobs: Enter the "Signing Bonus" Sweepstakes
http://hotjobs.sweepstakes.yahoo.com/signingbonus