🚀 go-pugleaf

Archive-name: theorem-provers/lindsay-survey
Original-posting-by: jon@cs.washington.edu (Jon Jacky)
Original-subject: Re: Summary of replies for PD theorem prover
Reposted-by: emv@math.lsa.umich.edu (Edward Vielmetti)

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