Introduction to HOL: A Theorem Proving Environment for Higher Order Logic

(1993)
  Copy   BIBTEX

Abstract

Higher-Order Logic (HOL) is a proof development system intended for applications to both hardware and software. It is principally used in two ways: for directly proving theorems, and as theorem-proving support for application-specific verification systems. HOL is currently being applied to a wide variety of problems, including the specification and verification of critical systems. Introduction to HOL provides a coherent and self-contained description of HOL containing both a tutorial introduction and most of the material that is needed for day-to-day work with the system. After a quick overview that gives a "hands-on feel" for the way HOL is used, there follows a detailed description of the ML language. The logic that HOL supports and how this logic is embedded in ML, are then described in detail. This is followed by an explanation of the theorem-proving infrastructure provided by HOL. Finally two appendices contain a subset of the reference manual, and an overview of the HOL library, including an example of an actual library documentation.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,069

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Symbolic logic and mechanical theorem proving.Chin-Liang Chang - 1973 - San Diego: Academic Press. Edited by Richard Char-Tung Lee.
Deduction: Automated Logic.W. Bibel, Steffen Hölldobler & Gerd Neugebauer - 1993 - London, England: Academic Press.

Analytics

Added to PP
2015-02-02

Downloads
19 (#696,820)

6 months
7 (#198,233)

Historical graph of downloads
How can I increase my downloads?

References found in this work

No references found.

Add more references