Sinossi
An introduction to the HOL theorem-proving system.
Le informazioni nella sezione "Riassunto" possono far riferimento a edizioni diverse di questo titolo.
Descrizione del libro
The HOL system aids the development of safety-critical software. The purpose here has been to provide a coherent and self-contained introduction to HOL and to extract and compress from various sources most of the material that is needed for day-to-day work with the system.
Contenuti
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.
Le informazioni nella sezione "Su questo libro" possono far riferimento a edizioni diverse di questo titolo.
Risultati della ricerca per Introduction to HOL: A Theorem-Proving Environment...
Immagini fornite dal venditore
Introduction to HOL a theorem proving environment for higher order logic ed.
Editore:
Cambridge, Cambridge University Press, 1993
ISBN 10: 0521441897
ISBN 13: 9780521441896
Antico o usato
Softcover
Da: Antiquariat Bookfarm, Löbnitz, Germania
Valutazione del venditore 5 su 5 stelle
Softcover. Ex-library with stamp and library-signature. GOOD condition, some traces of use. Ancien Exemplaire de bibliothèque avec signature et cachet. BON état, quelques traces d'usure. Ehem. Bibliotheksexemplar mit Signatur und Stempel. GUTER Zustand, ein paar Gebrauchsspuren. C 690 9780521441896 Sprache: Englisch Gewicht in Gramm: 550. Codice articolo 2498282
Compra usato
EUR 99,30
Spese di spedizione:
EUR 16,00
Da: Germania a: U.S.A.
Quantità: 1 disponibili
Foto dell'editore
Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic
Editore:
Cambridge University Press, 1993
ISBN 10: 0521441897
ISBN 13: 9780521441896
Nuovo
Rilegato
Prima edizione
Da: Anis Press, Walnut Creek, CA, U.S.A.
Valutazione del venditore 5 su 5 stelle
Hardcover. Condizione: New. 1st Edition. 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. Codice articolo 9780521441896
Compra nuovo
EUR 287,61
Spese di spedizione:
EUR 8,62
In U.S.A.
Quantità: 1 disponibili