**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

**Algorithmic Algebra**

by

**Bhubaneswar Mishra**-

**Courant Institute of Mathematical Sciences**

The main purpose of the book is to acquaint advanced undergraduate and graduate students in computer science, engineering and mathematics with the algorithmic ideas in computer algebra so that they could do research in computational algebra.

(

**17715**views)

**Mathematics for Algorithm and Systems Analysis**

by

**Edward A. Bender, S. Gill Williamson**-

**Dover Publications**

This text assists undergraduates in mastering the mathematical language to address problems in the field's many applications. It consists of 4 units: counting and listing, functions, decision trees and recursion, and basic concepts of graph theory.

(

**25306**views)

**Mathematical Illustrations: A Manual of Geometry and PostScript**

by

**Bill Casselman**-

**Cambridge University Press**

The author gives an introduction to basic features of the PostScript language and shows how to use it for producing mathematical graphics. The book includes the discussion computer graphics and some comments on good style in mathematical illustration.

(

**16325**views)

**Strange Attractors: Creating Patterns in Chaos**

by

**Julien C. Sprott**-

**M & T Books**

Chaos and fractals have revolutionized our view of the world. This book shows examples of the artistic beauty that can arise from very simple equations, and teaches the reader how to produce an endless variety of such patterns.

(

**16444**views)