Logo

Isabelle/HOL: A Proof Assistant for Higher-Order Logic

Large book cover: Isabelle/HOL: A Proof Assistant for Higher-Order Logic

Isabelle/HOL: A Proof Assistant for Higher-Order Logic
by

Publisher: Springer
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

Book cover: Computer Algebra, Algorithms, Systems and ApplicationsComputer Algebra, Algorithms, Systems and Applications
by - Czech Technical University
From the table of contents: Introduction; Algorithms for algebraic computation; Integrated mathematical systems; Basic possibilities of integrated mathematical systems; Applications of computer algebra; Another sources of study.
(12974 views)
Book cover: Mathematics for Algorithm and Systems AnalysisMathematics for Algorithm and Systems Analysis
by - Dover Publications
This text assists undergraduates in mastering the mathematical language to address problems in the field's many applications. It consists of 4 units: counting and listing, functions, decision trees and recursion, and basic concepts of graph theory.
(24652 views)
Book cover: Algorithms in Real Algebraic GeometryAlgorithms in Real Algebraic Geometry
by - 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.
(13569 views)
Book cover: Strange Attractors: Creating Patterns in ChaosStrange Attractors: Creating Patterns in Chaos
by - 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.
(15955 views)