Custom cover image
Custom cover image

Isabelle/HOL : A Proof Assistant for Higher-Order Logic / edited by Tobias Nipkow, Markus Wenzel, Lawrence C. Paulson

By: Contributor(s): Resource type: Ressourcentyp: Buch (Online)Book (Online)Language: English Series: SpringerLink Bücher | Springer eBook Collection Computer Science | Lecture notes in computer science ; 2283Publisher: Berlin, Heidelberg : Springer-Verlag Berlin Heidelberg, 2002Description: Online-RessourceISBN:
  • 9783540459491
  • 3540433767
Subject(s): Genre/Form: Additional physical formats: 9783540433767 | Buchausg. u.d.T.: Isabelle/HOL. Berlin : Springer, 2002. XIII, 218 S.MSC: MSC: *68T15 | 68-02 | 03B35RVK: RVK: ST 125 | SS 4800 | ST 304LOC classification:
  • QA8.9-QA10.3
DOI: DOI: 10.1007/3-540-45949-9Online resources: Summary: 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 systemPPN: PPN: 164926710XPackage identifier: Produktsigel: ZDB-2-BAE | ZDB-2-LNC | ZDB-2-SCS | ZDB-2-SXCS | ZDB-2-SEB
No physical items for this record
KIT – The University in the Helmholtz Association                         Home | Impressum | Datenschutz | Barrierefreiheit | KIT