|
Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel. Isabelle/HOL -- A Proof Assistant for Higher-Order Logic. LNCS 2283.
This book is a self-contained introduction to interactive proof in higher-order logic (HOL), using the proof assistant Isabelle2002. It is a tutorial for potential users rather than a monograph for researchers.
It is quite exciting to see how familiar functional programming constructs can be used directly inside a theorem prover. But beware, HOL is not the same as Haskell:
As we have indicated, the requirement for total functions is an essential characteristic
of HOL. It is only because of totality that reasoning in HOL is comparatively
easy. More generally, the philosophy in HOL is to refrain from asserting
arbitrary axioms (such as function definitions whose totality has not been proved)
because they quickly lead to inconsistencies. Instead, fixed constructs for introducing
types and functions are offered (such as datatype and primrec) which are
guaranteed to preserve consistency.
Still it is quite cool to see how much goes into proving that reverse(reverse(lst))=lst. For the detailed proof see chapter 2: Functional Programming in HOL.
Posted to Misc-Books by Ehud Lamm on 4/11/02; 3:57:52 AM
|
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
