********************************************* DESCRIPTION OF THE HOL THEOREM PROVING SYSTEM ********************************************* --------- KEYWORDS: --------- Higher Order, Classical, Natural deduction with tactics ----------------------------------------------------------------------------- ------------ DESCRIPTION: ------------ o *Semantics:* Classical higher order logic with Milner-style polymorphism o *Deductive machinery:* natural deduction proof system, with goal oriented deduction using the meta language ML for defining tactics and tacticals. o *Dynamics:* organized by theories -- signature, axioms, proved theorems. o *Persistence:* theories can be saved. Proofs are not (yet) saved, but the scripts that generated them are. The HOL system is an interactive environment for machine-assisted theorem-proving in higher-order logic. See for example: * M. Gordon.* ~ HOL: A proof generating system for higher-order logic.~ In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis. Kluwer, 1987. ----------------------------------------------------------------------------- ---------------- CONTACT PERSONS: ---------------- Email to [[]]. Alternatively contact one of the people listed below (see "Where-to-get-it"). ----------------------------------------------------------------------------- ----------- USER GROUP: ----------- The HOL user group is [[]]. To join, send email to [[]] HOL is currently in use at companies, government organizations and higher education institutions in North America, Europe, China and Japan. It is used for hardware verification, software verification, proof-checking pure mathematics and basic research into machine-assisted formal proof. ----------------------------------------------------------------------------- ----------- PRAGMATICS: ----------- --------- STRENGTH: --------- The HOL logic is simple but expressive, incorporating higher-order functions and Milner-style polymorphism. HOL uses the programming language ML to program proof strategies. Theorems are encoded via an abstract type whose only constructors are the primitive inference rules of the logic. Other proof strategies ultimately resolve into these steps. This combines a high degree of security with great flexibility: the user can safely extend the inference system without being a logician. A large number of derived rules have been programmed for, e.g., proving facts in linear arithmetic, defining recursive datatypes or handling inductive definitions. (The large user base contributes to the stock of derived rules.) Backward (goal-directed) proof is supported, and may be freely mixed with forward proof. Adherence to definitional extension guarantees that the consistency of the logic is not compromised. ----------- WEAKNESSES: ----------- Some features of other type systems such as subtypes and dependent types are not supported, although research is in progress regarding ways of embedding them in the basic logic. The insistence on resolving proofs into simple primitive inferences can make HOL slow. Some common proof strategies have not (yet) been automated by derived rules, necessitating some rather low-level guidance by the user. ----------------------------------------------------------------------------- -------------- DOCUMENTATION: -------------- Full machine-readable (LaTeX) documentation is supplied with HOL. This includes the four volumes of the system manual: o [[Tutorial]] -- Introduction to installing and using HOL o [[Description]] -- ML, semantics of HOL, derived rules and tactics o [[Reference]] -- reference for everything in the system o [[Libraries]] -- documentation for libraries outside the core In addition, the release contains various case studies and LaTeX sources of slides for a training course. The following book will be available in early 1993: ~Introduction to HOL~ M. J. C. Gordon & T. F. Melham (eds.) Cambridge University Press 1993 ISBN 0-521-441897 For details of HOL see: [[]] Training courses are organized periodically: contact Inder Dhingra (isd@cl.cam.ac.uk) for more details. ----------------------------------------------------------------------------- ------------- APPLICATIONS: ------------- HOL has been used for a wide variety of purposes, including the verification of hardware, software and protocols, as well as proof-checking mathematics. An account of using the HOL system to partially verify the commercially-available VIPER microprocessor is given in: *Avra Cohn* ~"The Notion of Proof in Hardware Verification"~ Journal of Automated Reasoning, Vol. 5, May 1989, pp. 127-139 The verification of another microprocessor, of a more "functional" style, is reported in the following book: *Brian T. Graham* ~The SECD Microprocessor: A verification case study~ Kluwer 1992 ISBN 0-7923-9245-0 The verification of a larger microcoded microprocessor is reported in: *Phillip J. Windley* ~[["Formal Modelling and Verification of Microprocessors"]]~ IEEE Transactions on Computers, Vol 44(1), January 1995, pp. 54-72. The verification of a pipelined microprocessor is reported in: *Phillip J. Windley* ~[["A Correctness Model for Pipelined Microprocessors"]]~ Proceedings of TPCD 94, Bad Herrenalb, Germany. Springer-Verlag Lecture Notes in Computer Science No. 901, September, 1994. ----------------------------------------------------------------------------- -------------------------- CONFERENCES AND WORKSHOPS: -------------------------- There is a yearly conference on the HOL theorem proving system and its applications. The folowing proceedings are available. More information about [[venues and future conferences]] is also available. o ~Proceedings of the 1991 International Workshop on the HOL theorem proving system and its applications, Davis, California.~ Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley (eds.) IEEE Computer Society Press 1992 ISBN 0-8186-2460-4 (paper) o ~Higher Order Logic Theorem Proving and Its Applications. Proceedings of the 1992 International Workshop on Higher Order Logic Theorem Proving and its Applications, Leuven, Belgium.~ Luc J. M. Claesen, Michael J. C. Gordon (eds.) North-Holland, Amsterdam, The Netherlands 1993 ISBN 0 44 89880 8 o ~Proceedings of the 1993 International Workshop on Higher Order Logic Theorem Proving and its Applications, UBC, Vancouver, Canada.~ Jeffrey J. Joyce, Carl Seger (eds.) Springer-Verlag Lecture Notes in Computer Science No. 780, 1993. o ~Proceedings of the 1994 International Workshop on Higher Order Logic Theorem Proving and its Applications, Valletta, Malta.~ Thomas F. Melham, Juanito Camilleri (eds.) Springer-Verlag Lecture Notes in Computer Science No. 859, 1994. ~HOL around the World~, a document describing HOL projects (complete, on going, beginning) is included with the HOL release. ----------------------------------------------------------------------------- ------------------------ EXTENSIONS/ENHANCEMENTS: ------------------------ A color interface is under development using Centaur in collaboration with Inria, Sophia Antipolis, France. ----------------------------------------------------------------------------- ---------------------- RESOURCE REQUIREMENTS: ---------------------- Workstation running Common Lisp or SML. ----------------------------------------------------------------------------- ---------------- WHERE-TO-GET-IT: ---------------- There are actually [[three HOL systems:]] 1. Classic HOL (also called HOL88) -- this is the one described above. 2. HOL90 from Calgary, written in Standard ML. Also public domain. 3. ICL HOL. A commercial product from ICL. This is used to support reasoning about Z. The Classic HOL system is available as a public domain system from the following FTP sites: ftp.cl.cam.ac.uk [128.232.0.56] in directory "[[hvg/hol]]" lal.cs.byu.edu [128.187.2.182] in directory "[[pub/hol]]" The two main files are "holsys.tar.gz" and "holdoc.tar.gz", which are compressed tarfiles of, respectively, the hol system (i.e. code, theories) and the hol documentation (help files and stuff to build the manuals). The file "gzip-1.2.4.tar" has code to uncompress .gz files. There are other odds and ends available too, mostly concerned with particular LISPs. HOL can also be supplied on magnetic tape for the benefit of users without FTP access. Contact "hol-support@cl.cam.ac.uk" for more details, or one of: John Harrison University of Cambridge Computer Laboratory New Museums Site Pembroke Street Cambridge CB2 3QG England. jrh@cl.cam.ac.uk [[Phillip J. Windley]] , Asst. Professor Laboratory for Applied Logic Department of Computer Science Brigham Young University Provo, UT 84602-6576 <[[windley@lal.cs.byu.edu]]> ~Updated Fri Sep 6 09:15:57 1996 ~** by [[Paul E. Black]] ([[black@cs.byu.edu]]) [[[IMAGE(button-home.gif)] ]] Back to the documentation menu.