Isabelle/HOL: A Proof Assistant for Higher-Order Logic
by T. Nipkow, L.C. Paulson, M. Wenzel
Publisher: Springer 2010
Number of pages: 223
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:
by Thomas Hales - arXiv
Computers have rapidly become so pervasive in mathematics that future generations may look back to this day as a golden dawn. The article gives a survey of mathematical proofs that rely on computer calculations and formal proofs.
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.
by 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.
by 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.