Isabelle/HOL

出版者:Springer; 1 edition

页数:218 页

出版时间:2002年

价格:110.0

装帧:平装

isbn号码:9787835404333

图书标签:计算机编程数学Programming

在线阅读本书

This textbook-like tutorial is a self-contained introduction to interactive proof, specification, and verification in higher-order logic, using the proof assistant Isabelle 2002. In contrast to existing Isabelle documentation, this book provides a direct route into higher-order logic by bypassing first-order logic and minimizing discussion of meta-theory.

Isabelle is a generic system for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for higher-order logic; this theorem prover is well suited as a specification and verification system.