000			00644nam a2200217Ia 4500
999			_c6194 _d6194
008			161214s9999 xx 000 0 und d
020			_a3540433767 _cpbk
082			_a004 _bNIP
100			_aPaulson, Lawrence C.
245		0	_aIsabelle/HOL : a Proof Assistant for Higher-Order Logic
260			_aBerlin: _bSpringer-Verlag, _c2002
300			_axiii, 218 p.; _b: _c24 cm.
365			_aINR _b2059.20/ EURO 33.00
440			_v2283
490			_aLecture notes in computer science
520			_aThis 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.
650			_aAutomatic theorem proving
650			_aComputer logic
650			_aProgramming in HOL
650			_aConcrete syntax
650			_aSets, Function & Relations
650			_aTuples
650			_aSimplification, recursion & induction
650			_aSecurity protocol
650			_aArtificial intelligence
650			_aLogic & sets
700			_aNipkow, Tobias
700			_aWenzel, Markus
700			_aPaulson, Lawrence C.
942			_2ddc _cBK