Isabelle/HOL : a Proof Assistant for Higher-Order Logic
- Berlin: Springer-Verlag, 2002
- xiii, 218 p.; : 24 cm.
- 2283 .
- Lecture notes in computer science .
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.
3540433767 pbk
Automatic theorem proving Computer logic Programming in HOL Concrete syntax Sets, Function & Relations Tuples Simplification, recursion & induction Security protocol Artificial intelligence Logic & sets