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
Mathematics for Computer Scientistsby Gareth J. Janacek, Mark L. Close - BookBoon
In this textbook you will find the basic mathematics needed by computer scientists. It should help you to understand the meaning of mathematical concepts. Subjects as elementary logic, factorization, plotting functions and matrices are explained.
(28848 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.
(10886 views)
Implementing Mathematics with The Nuprl Proof Development Systemby 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.
(18530 views)
Probabilistic Programming and Bayesian Methods for Hackersby 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.
(24301 views)