Xref: utzoo comp.ai:5295 comp.lang.lisp:2609 comp.lang.lisp.x:53 comp.theory:137 sci.math:9096 sci.math.symbolic:1064
Path: utzoo!utgpu!jarvis.csri.toronto.edu!rutgers!mit-eddie!uw-beaver!uw-june!jon
From: jon@cs.washington.edu (Jon Jacky)
Newsgroups: comp.ai,comp.lang.lisp,comp.lang.lisp.x,comp.theory,sci.math,sci.math.symbolic
Subject: Re: Summary of replies for PD theorem prover
Summary: Review article discusses many provers
Message-ID: <10243@june.cs.washington.edu>
Date: 28 Dec 89 18:18:32 GMT
References: <647@uncle.UUCP>
Organization: U of Washington, Computer Science, Seattle
Lines: 15

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