Isabelle/HOL. A proof assistant for higher-order logic. (English) Zbl 0994.68131

Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus

Lecture Notes in Computer Science. 2283. Berlin: Springer. xiii, 218 p. (2002).

Publisher’s description: 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.

MSC:

68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
68-02	Research exposition (monographs, survey articles) pertaining to computer science
03B35	Mechanization of proofs and logical operations

Keywords:

Isabelle

Software:

Isabelle; HOL; Isabelle/HOL; Haskell; Proof General