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.
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.
NQTHM started as the Boyer Moore theorem prover. (U Texas,
same school as Bill Schelter).
OTTER is from Argonne National Labs.
RJF
C Y wrote:
>--- Stavros Macrakis <stavros.macrakis@verizon.net> wrote:
>
>
>>>That would be a very interesting addition to Maxima. Otter
>>>is coded in ANSI C, presumably for speed, so I have no idea
>>>how much work a lisp reimplimentation would be.
>>>
>>>
>>Why would you want to reimplement it rather than interface to it as a
>>black box? Even if the various Lisps don't have a good story on
>>native code interfaces, it should be possible to write a socket
>>interface, no?
>>
>>
>
>I suppose, if Otter can communicate by sockets. I guess personally I
>figure that if the system is implimented as part of Maxima, it would be
>much easier to customize it's abilities and interaction environment to
>work smoothly with the rest of the system. Any external package
>introduces three immediate complications:
>
>1) What platforms does it run on? Will some Maxima platform get short
>changed?
>
>2) Who is maintaining it? Even if it runs on many systems now, will
>it continue to do so in the future?
>
>3) Is the syntax/api/whatever stable? If a current version of
>something already has all the features it makes sense to add to Maxima,
>there is a risk that future versions might be incompatible, and we
>would have to write code to attempt to account for different versions.
>Yech.
>
>Of course, I am not trying to say there aren't cases where a foreign
>function interface or socket communication is the more logical choice.
>But it is pretty much a fact of life that the less self contained a
>program is, the harder it is to keep it working. Gnome and KDE
>applications have this problem all the time - they must stay current
>with other software or be crippled. Their apps are usually main stream
>enough to make it work, but on something like Maxima where one or two
>qualified people might do a lot of work and no one else looks at it for
>years after it becomes part of the working system, the case for self
>contained, well defined components merits thought. The tremendous
>downside is of course reimplimenting all the work already done, and I
>agree it is a severe downside.
>
>CY
>