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
The Life of Pi: From Archimedes to Eniac and Beyondby Jonathan M. Borwein - DocServer
The desire to understand Pi, the challenge, and originally the need, to calculate ever more accurate values of Pi, has challenged mathematicians for many many centuries, and Pi has provided compelling examples of computational mathematics.
(22535 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.
(11703 views)
An Architecture for Combinator Graph Reductionby Philip J. Koopman, Jr. - Academic Press
The results of cache-simulation experiments with an abstract machine for reducing combinator graphs are presented. The abstract machine, called TIGRE, exhibits reduction rates that compare favorably with previously reported techniques.
(19466 views)
Curves and Surfaces in Geometric Modeling: Theory and Algorithmsby Jean Gallier - Morgan Kaufmann
This book offers both a theoretically unifying understanding of polynomial curves and surfaces and an effective approach to implementation that you can bring to bear on your own work -- whether you are a graduate student, scientist, or practitioner.
(9410 views)