jbn@FORD-WDL1.ARPA (05/25/84)
[Forwarded from the Stanford bboard by Laws@SRI-AI.]
The Boyer-Moore prover is now available for UNIX systems. While I
did the port, Boyer and Moore now have my code and have integrated it
into their generic version of the prover. They are handling distribution.
The prover is now available for the Symbolics 3600, TOPS-20 systems,
Multics, and UNIX for both VAXen and SUNs. There is a single version with
conditional compilation, it resides on UTEXAS-20, and can be obtained via
FTP. Send requests to BOYER@UTEXAS-20 or MOORE@UTEXAS-20, not me, please.
The minimum machine for the prover is a 2MB UNIX system with Franz Lisp
38.39 or later, about 20-80MB of disk, and plenty of available CPU time.
If you want to know more about the prover, read Boyer and Moore's
``A Computational Logic'' (1979, Academic Press, ISBN 0-12-122950-5).
Using the prover requires a thorough understanding of this work.
Please pass this on to all who got the last notice, especially
bulletin boards and news systems. Thanks.
Nagle (@SCORE)