From: Steve K. Roggenkamp
Subject: Summary of replies for PD theorem prover
Date:
Message-ID: <647@uncle.UUCP>
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 <·······@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 (·····@albanycs.albany.edu and Hantao Zhang
(······@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, ···@uncle.UUCP, ···············@osu-cis.cis.ohio-state.edu
(614) h:792-8236, w:764-4208;
--
-----
Steven K. Roggenkamp, ···@uncle.UUCP, ···············@osu-cis.cis.ohio-state.edu
(614) h:792-8236, w:764-4208;
On the subject of PD theorem provers, let me mention one that I use in my
research called HOL. HOL is based on typed lambda calculus and is in the
LCF family of theorem provers meaning that it has a meta--language (ML)
making it programmable and supports both backwards (goal oriented) and
forward proof styles. HOL was written by Mike Gordon at the University of
Cambridge.
HOL has a large user community and is being used around the world for a
number of commercial and academic research programs both in computer
systems specification and verification. HOL is written in Lisp and is
available on a large number of processors. You can get a copy via
anonymous ftp from clover.ucdavis.edu. If you'd like more information on
HOL, contact me or have a look at the article by Mike Gordon "HOL: A Proof
Generating System for Higher Order Logic," from VLSI Specification,
Verification, and Synthesis, G. Birtwhistle and P. Subrahmanyam (eds.),
Kluwer, 1987. (I can make a postscript copy of this article available to
those who are interested.)
--
Phil Windley | ·······@cheetah.ucdavis.edu
Division of Computer Science | ucbvax!ucdavis!cheetah!windley
College of Engineering | (916) 752-6452 (or 3168)
University of California, Davis | Davis, CA 95616
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
···@gaffer.rad.washington.edu
From: earl
Subject: Re: Summary of replies for PD theorem prover
Date:
Message-ID: <3607@ccncsu.ColoState.EDU>