Xref: utzoo comp.lang.lisp:2607 sci.math:9089 Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!uunet!tut.cis.ohio-state.edu!ucbvax!ucdavis!ucdavis.ucdavis.edu!windley From: windley@cheetah.ucdavis.edu (Phil Windley/20000000) Newsgroups: comp.lang.lisp,sci.math Subject: Re: PD theorem provers Message-ID: Date: 27 Dec 89 17:59:54 GMT References: <647@uncle.UUCP> Sender: uucp@ucdavis.ucdavis.edu Organization: UCD Robotics Research Lab Lines: 28 In-reply-to: skr@uncle.UUCP's message of 27 Dec 89 03:23:07 GMT 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