[sci.math.symbolic] Summary of replies for PD theorem prover

skr@uncle.UUCP (Steve K. Roggenkamp) (12/27/89)

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;  

jon@cs.washington.edu (Jon Jacky) (12/29/89)

A review of many theorem-proving systems appears in an article in the British
periodical, SOFTWARE ENGINEERING JOURNAL, vol 3 no 1, Jan 1988: "A Survey of 
Mechanical Support for Formal Reasoning" by Peter A. Lindsay.

This review discusses the following systems at length: LCF, NuPRL, Veritas,
Isabelle, Affirm, the Boyer-Moore Prover, and the Gypsy Verification 
Environment.  He also briefly discusses Abstract Pascal, B, the CSG proof 
editor, enhanced HDM, FDM, HOL, Interactive Proof Editor, IOTA, NEVER, REVE,
and the Stanford Pascal Verifier.

I seem to recall that he discusses avialability, public domain or otherwise,
for each of these systems.

- Jonathan Jacky, University of Washington, Seattle, WA 
  jon@gaffer.rad.washington.edu

crussell@handel.CS.ColoState.Edu (earl) (01/07/90)

   test!