Introduction to HOL

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.

ISBN 0521441897   DEWEY edition DC20 ISBN13 9780521441896 (What's this?)   Pages 492 Publisher Cambridge University Press   Volumes 1 Imprint Cambridge University Press   Weight (grammes) 739 Format Hardback   Published in Cambridge Publication date 18 Mar 1993   Height (mm) 228 Non-book description xx, 472 p. :   Width (mm) 152 Library of Congress QA76.9.A96 I6 1993   Spine width (mm) 27 DEWEY 511.3028553   Academic level Professional / Scholarly

		Preface
Pt. I		Tutorial		1
1		Introduction to ML		3
2		Overview of the HOL Logic		9
3		Introduction to Proof with HOL		23
4		Introduction to Goal Directed Proof		33
5		Example: a Simple Parity Checker		47
6		How to Program a Proof Tool		61
7		Example: the Binomial Theorem		77
Pt. II		The Meta-language ML		97
8		Introduction and Examples		99
9		Syntax of ML		117
10		Semantics of ML		125
11		ML Types		135
12		Primitive ML Identifier Bindings		149
13		General Purpose and List Processing Functions		153
14		ML System Functions		167
Pt. III		The HOL Logic		191
15		Syntax and Semantics		193
16		Theories		209
Pt. IV		The HOL System		233
17		Syntax of the Logic in ML		235
18		Theorems and Theories		255
19		The Built-in Theories of HOL		277
20		The Type Definition Package		295
21		Miscellaneous System Features		309
Pt. V		Theorem Proving with HOL		321
22		Derived Inference Rules		323
		More...

..".an excellent presentation of a sophisticated reasoning system." Computing Reviews

 Be the first to write a customer review