🚀 go-pugleaf

Archive-name: hol/how-to-get
Original-posting-by: windley@cheetah.ucdavis.edu (Phil Windley/20000000)
Original-subject: Re: PD theorem provers
Archive-site: clover.ucdavis.edu [128.120.57.1]
Reposted-by: emv@math.lsa.umich.edu (Edward Vielmetti)


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                          |  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