Umfang:
Online-Ressource
ISBN:
9783540459491
,
3540433767
Serie:
Lecture Notes in Computer Science 2283
Inhalt:
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
Weitere Ausg.:
ISBN 9783540433767
Weitere Ausg.:
Buchausg. u.d.T. Nipkow, Tobias, 1958 - Isabelle/HOL Berlin : Springer, 2002 ISBN 3540433767
Sprache:
Englisch
Fachgebiete:
Informatik
Schlagwort(e):
HOL
;
Isabelle
;
HOL
;
Funktionale Programmierung
;
HOL
;
Formale Methode
;
Aufsatzsammlung
DOI:
10.1007/3-540-45949-9
URL:
Volltext
(lizenzpflichtig)
URL:
Volltext
(lizenzpflichtig)
Mehr zum Autor:
Nipkow, Tobias 1958-
