Isabelle/HOL

A Proof Assistant for Higher-Order Logic

Versandkostenfrei!
Versandfertig in 1-2 Wochen
43,99 €
inkl. MwSt.
Weitere Ausgaben:
PAYBACK Punkte
22 °P sammeln!
This volume is a self-contained introduction to interactive proof in high- order logic (HOL), using the proof assistant Isabelle 2002. Compared with existing Isabelle documentation, it provides a direct route into higher-order logic, which most people prefer these days. It bypasses ?rst-order logic and minimizes discussion of meta-theory. It is written for potential users rather than for our colleagues in the research world. Another departure from previous documentation is that we describe Markus Wenzel s proof script notation instead of ML tactic scripts. The l- ter make it easier to introduc...