skr@uncle.UUCP (Steve K. Roggenkamp) (12/29/89)
Archive-name: theorem-provers/skr-summary Original-posting-by: skr@uncle.UUCP (Steve K. Roggenkamp) Original-subject: Summary of replies for PD theorem prover Archive-site: herky.cs.uiowa.edu [128.255.28.100] Archive-directory: public/otter Archive-files: README Reposted-by: emv@math.lsa.umich.edu (Edward Vielmetti) 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;