jon@cs.washington.edu (Jon Jacky) (12/29/89)
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