Xref: utzoo comp.ai:5289 comp.lang.lisp:2605 comp.lang.lisp.x:52 comp.theory:134 sci.math:9087 sci.math.symbolic:1060
Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!wuarchive!zaphod.mps.ohio-state.edu!tut.cis.ohio-state.edu!n8emr!uncle!skr
From: skr@uncle.UUCP (Steve K. Roggenkamp)
Newsgroups: comp.ai,comp.lang.lisp,comp.lang.lisp.x,comp.theory,sci.math,sci.math.symbolic
Subject: Summary of replies for PD theorem prover
Message-ID: <647@uncle.UUCP>
Date: 27 Dec 89 03:23:07 GMT
Reply-To: skr@uncle.UUCP (Steve K. Roggenkamp)
Organization: U.N.C.L.E.
Lines: 40

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;