Isabelle/HOL : a Proof Assistant for Higher-Order Logic
By: Paulson, Lawrence C.
Contributor(s): Nipkow, Tobias | Wenzel, Markus | Paulson, Lawrence C.
Material type:
BookSeries: 2283. Lecture notes in computer science.Publisher: Berlin: Springer-Verlag, 2002Description: xiii, 218 p.; : 24 cm.ISBN: 3540433767 .Subject(s): Automatic theorem proving | Computer logic | Programming in HOL | Concrete syntax | Sets, Function & Relations | Tuples | Simplification, recursion & induction | Security protocol | Artificial intelligence | Logic & setsDDC classification: 004 Summary: This textbook-like tutorial is a self-contained introduction to interactive proof, specification, and verification in higher-order logic, using the proof assistant Isabelle 2002. In contrast to existing Isabelle documentation, this book provides a direct route into higher-order logic by bypassing first-order logic and minimizing discussion of meta-theory. Isabelle is a generic system for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for higher-order logic; this theorem prover is well suited as a specification and verification system.
| Item type | Current location | Call number | Status | Date due | Barcode |
|---|---|---|---|---|---|
| Books | 004 NIP (Browse shelf) | Available | 011975 |
This textbook-like tutorial is a self-contained introduction to interactive proof, specification, and verification in higher-order logic, using the proof assistant Isabelle 2002. In contrast to existing Isabelle documentation, this book provides a direct route into higher-order logic by bypassing first-order logic and minimizing discussion of meta-theory. Isabelle is a generic system for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for higher-order logic; this theorem prover is well suited as a specification and verification system.
There are no comments for this item.