1 option
Isabelle/HOL : a proof assistant for higher-order logic / Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel.
LIBRA QA76.9.L63 N53 2002
Available from offsite location
- Format:
- Book
- Author/Creator:
- Nipkow, Tobias, 1958-
- Series:
- Lecture notes in computer science ; 2283.
- Lecture notes in computer science ; 2283
- Language:
- English
- Subjects (All):
- Computer logic.
- Automatic theorem proving.
- Physical Description:
- xiii, 218 pages : illustrations ; 24 cm.
- Place of Publication:
- Berlin ; New York : Springer, [2002]
- 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.
- Notes:
- Includes bibliographical references (pages [209]-211) and index.
- ISBN:
- 3540433767
- OCLC:
- 49320458
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.