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!