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
Art Gallery Theorems and Algorithmsby Joseph O'Rourke - Oxford University Press
Art gallery theorems and algorithms are so called because they relate to problems involving the visibility of geometrical shapes and their internal surfaces. This book explores generalizations and specializations in these areas.
(23990 views)
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.
(30364 views)
Think Stats: Probability and Statistics for Programmersby Allen B. Downey - Green Tea Press
Think Stats is an introduction to Probability and Statistics for Python programmers. This new book emphasizes simple techniques you can use to explore real data sets and answer interesting statistical questions. Basic skills in Python are assumed.
(27259 views)
Vector Math for 3D Computer Graphicsby Bradley Kjell - Central Connecticut State University
A text on vector and matrix algebra from the viewpoint of computer graphics. It covers most vector and matrix topics needed for college-level computer graphics text books. Useful to computer science students interested in game programming.
(25717 views)