windley@cheetah.ucdavis.edu (Phil Windley/20000000) (12/28/89)
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