feature request for "NOT" // theorem prover?

This has gotten somewhat off track for the subject, but
(1) Nqthm runs in the maxima image, if you want a theorem prover.  
Presumably
this is different from Otter in a variety of ways, but at the level of 
discussion here,
you can consider them equivalent, I think.

(2) If the system you are linking to from lisp is itself interactive and 
maintains variable
"state"  and has a need to be interrupted etc., then the communication 
can be messy.
If it is "functional"  e.g.  as is typical for a bignum package like 
GMP, or an image
file-reading package to read in TIFF files,  or a Fortran program to do 
numerical
integration, then communication is not messy. It really really helps if 
the program you
are linking to is not changing every 2 weeks.

I don't know how the theorem provers need to work, but nqthm seems to do
approximately this:
You set up a file with axioms and such stuff, and a theorem to prove.
You call the theorem prover and it produces a proof, presumably on your
standard output or on a file, in text or TeX,    or  <not true>.

So this seems to be "functional" unless you want to make it quit...
RJF


CY wrote:

>On Fri, 9 Jan 2004 18:17:17 -0500
>"Stavros Macrakis" <stavros.macrakis@verizon.net> wrote:
>
>  
>
>>If you have two sources, then you must port any bug reports, test
>>suites, bug fixes, and enhancements from one to the other, one item at a
>>time. 
>>    
>>
>
>Only if we are using the original program exactly as intended.  For example, my guess would be that converting NQTHM or Otter to do what we want in Maxima would involve starting with the original code base and adapting it to the Maxima environment.  Perhaps it would be easier than that, but I would be rather surprised if that's the case.  If we are using a subset or heavily modified version it is unlikely that all developments to the original program would be of interest or relevant to Maxima's use of the code, although of course bug reports and fixes would always merit watching.
>
>  
>
>>If of course the other package is no longer being maintained,
>>then this is irrelevant -- but in that case there is also no danger of
>>new incompatibilities.
>>    
>>
>
>Not between Maxima and the package, of course, but between the package and new versions of Windows|Linux|MacOSX|compiler|etc. the chance is still there, and if the package must be fixed we must become maintainers.  This is why we can't use IZIC currently, for example.
>
>  
>
>>Personally, I do always like to have source in Lisp because I am more
>>comfortable in the Lisp environment than any other one.  But I should
>>learn to deal better with other systems.  Oh, and systems in general
>>should learn to "play together" better -- Maxima of course being as bad
>>as other systems this way.
>>    
>>
>
>Dr. Fateman can speak to this much better than I can, but in general isn't there some kind of problem with systems communicating because the environment of the "dominant" system and the other systems involved can't share enough information to be sure that manipulations of data not allowed in the original environment pass in the other system's own environment?  Of course, there are trivial cases where it can work, but I thought one of the major merits of reimplimenting abilities for Maxima was that we have access to the Maxima system state.  I could be wrong though.
>
>  
>
>>It is also not clear that a Lisp version of Otter would actually be
>>enhanced at all -- will we attract theorem-prover hackers to the Lisp
>>version?  If we do want a Lisp-based theorem prover, perhaps it would be
>>better to find an existing one....
>>    
>>
>
>I guess that depends on what we want to use Otter for.  I'm not sure the question can be answered until it's clear what parts we want and what jobs we want them to do.
>
>  
>
>>I also wonder how much of a performance hit one would get by moving from
>>C to Lisp.  Theorem provers are slow, I think, so a factor of 5 or 10 or
>>50 in speed could make a real practical difference.
>>    
>>
>
>It could be, I suppose.  But there again, it probably depends on what we want to ask it to do.
>
>CY
>
>_______________________________________________
>Maxima mailing list
>Maxima@www.math.utexas.edu
>http://www.math.utexas.edu/mailman/listinfo/maxima
>  
>