ENGLISH

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

By M. J. C. Gordon , T. F. Melham

Book information

Publisher
Cambridge University Press
Year
1993
ISBN
0521441897, 9780521441896
LCC
QA76.9.A96 I6 1993
Open Library ID
OL1161377M
Language
english
Format
DJVU
Filesize
3 MB (3208565 bytes)
Edition
Spi
Pages
493\493
Topic
Mathematics Logic
Library
Kolxo3
DPI
600
Time added
2011-01-06 10:13:16

Description

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.

Similar books