Introduction to HOL
A Theorem-Proving Environment for Higher-Order Logic
Published on 18. March 1993
Book
Hardback
492 pages
978-0-521-44189-6 (ISBN)
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.
More details
Language
English
Place of publication
Cambridge
United Kingdom
Target group
Professional and scholarly
Dimensions
Height: 226 mm
Width: 165 mm
Thickness: 27 mm
Weight
739 gr
ISBN-13
978-0-521-44189-6 (9780521441896)
Copyright in bibliographic data and cover images is held by Nielsen Book Services Limited or by the publishers or by their respective licensors: all rights reserved.
Schweitzer Classification
Persons
Content
Part I. Tutorial: 1. Introduction to ML; 2. The HOL logic; 3. Introduction to proof with HOL; 4. Goal-oriented proof: tactics and tacticals; 5. Example: a simple parity checker; 6. How to program a proof tool; 7. Example: the binomial theorem; Part II. The Meta-Language ML: 8. The history of ML; 9. Introduction and examples; 10. Syntax of ML; 11. Semantics of ML; 12. ML types; 13. Primitive ML identifier bindings; 14. General purpose and list processing functions; 15. ML system functions; Part III. The Hol Logic: 16. Syntax and semantics; 17. Theories; Part IV. The Hol System: 18. The HOL logic in ML; Part V. Theorem-Proving With HOL: 19. Derived inference rules; 20. Conversions; 21. Goal-directed proof: tactics and tacticals; Appendices.