Isabelle/HOL : a proof assistant for higher-order logic
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...
Shranjeno v:
| Auteurs principaux: | , , |
|---|---|
| Format: | Livre numérique |
| Jezik: | Anglais |
| Izdano: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serija: | Lecture notes in computer science
2283 |
| Teme: | |
| Online dostop: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Sporočilo: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Isabelle/HOL, a proof assistant for higher-order logic, Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel, 2002, Berlin, Springer, 1 vol. (XIII-218 p.), Lecture notes in computer science, 3-540-43376-7 • Isabelle/HOL, Texte imprimé, 9783662182291 |
Kazalo:
- Elementary Techniques
- 1. The Basics
- 2. Functional Programming in HOL
- 3. More Functional Programming
- 4. Presenting Theories
- Logic and Sets
- 5. The Rules of the Game
- 6. Sets, Functions, and Relations
- 7. Inductively Defined Sets
- Advanced Material
- 8. More about Types
- 9. Advanced Simplification, Recursion, and Induction
- 10. Case Study: Verifying a Security Protocol.