🚀 go-pugleaf

Thanks to all who replied to my request for a public domain theorem
prover.

Several people wrote about the Otter system developed at Argonne
National Labs by Bill McCune.  This system has the advantages of being
written in C and is fast.  It is available from two sites,
herky.cs.uiowa.edu and dopey.cs.unc.edu.  Instructions to obtain,
provided by Joachim Posegga <posegga@ira.uka.de> are:

>Otter is obtainable from herky.cs.uiowa.edu  username anonymous, 
>password guest, go to public/otter and follow the directions in README.

>dopey.cs.unc.edu  username anonymous, password guest, go to pub/Otter 
>and follow the directions in README.

Werner Vogels (relay.EU.net!nikhefk!werner) mentioned the Rule Rewrite
Laboratory (RRL), an interactive system developed at Iowa University
by Deepak Kapur (kapur@albanycs.albany.edu and Hantao Zhang
(hzhang@herky.cs.uiowa.edu).

My own personal interest in this area is using a theorem prover as an
aid for formal program specifications and to become more familiar with
this area of computer science.  It seems a theorem prover should be
useful for this purpose, although I do not have any experience in
using them.  I would like to use it to assist me with the details of
checking software specifications, but I'm leery of the amount of
detail they might spew forth.  The only way I can judge the usefulness
of this approach is to try it and evaluate the results.  If I find
something useful, I'll post it to the net.

Thanks again to all who replied.

Steve R.
-----
Steven K. Roggenkamp, skr@uncle.UUCP, n8emr!uncle!skr@osu-cis.cis.ohio-state.edu
(614) h:792-8236, w:764-4208;  
-- 
-----
Steven K. Roggenkamp, skr@uncle.UUCP, n8emr!uncle!skr@osu-cis.cis.ohio-state.edu
(614) h:792-8236, w:764-4208;