**Isabelle/HOL: A Proof Assistant for Higher-Order Logic**

by T. Nipkow, L.C. Paulson, M. Wenzel

**Publisher**: Springer 2010**ISBN/ASIN**: 3540433767**ISBN-13**: 9783540433767**Number of pages**: 223

**Description**:

This book is a self-contained introduction to interactive proof in higher-order logic (HOL), using the proof assistant Isabelle. It is a tutorial for potential users rather than a monograph for researchers. The book has three parts: Elementary Techniques; Logic and Sets; Advanced Material.

Download or read it online for free here:

**Download link**

(1.2MB, PDF)

## Similar books

**Implementing Mathematics with The Nuprl Proof Development System**

by

**R. L. Constable, at al.**-

**Prentice Hall**

The authors offer a tutorial on the new mathematical ideas which underlie their research. Many of the ideas in this book will be accessible to a well-trained undergraduate with a good background in mathematics and computer science.

(

**17784**views)

**A Computational Introduction to Number Theory and Algebra**

by

**Victor Shoup**-

**Cambridge University Press**

This introductory book emphasises algorithms and applications, such as cryptography and error correcting codes. It is accessible to a broad audience. Prerequisites are a typical undergraduate course in calculus and some experience in doing proofs.

(

**42393**views)

**Vector Math for 3D Computer Graphics**

by

**Bradley Kjell**-

**Central Connecticut State University**

A text on vector and matrix algebra from the viewpoint of computer graphics. It covers most vector and matrix topics needed for college-level computer graphics text books. Useful to computer science students interested in game programming.

(

**23035**views)

**Probabilistic Programming and Bayesian Methods for Hackers**

by

**Cameron Davidson-Pilon**-

**GitHub, Inc.**

This book is designed as an introduction to Bayesian inference from a computational understanding-first, and mathematics-second, point of view. The book assumes no prior knowledge of Bayesian inference nor probabilistic programming.

(

**23503**views)