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
Algorithms in Real Algebraic Geometryby S. Basu, R. Pollack, M. Roy - Springer
The monograph gives a detailed exposition of the algorithmic real algebraic geometry. It is well written and will be useful both for beginners and for advanced readers, who work in real algebraic geometry or apply its methods in other fields.
(21107 views)
Strange Attractors: Creating Patterns in Chaosby 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.
(23855 views)
Numerical Algorithms: Methods for Computer Vision, Machine Learning, and Graphicsby Justin Solomon - CRC Press
Using examples from a broad base of computational tasks, including data processing and computational photography, the book introduces numerical modeling and algorithmic design from a practical standpoint and provides insight into theoretical tools.
(12481 views)
Mathematical Illustrations: A Manual of Geometry and PostScriptby 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.
(24186 views)