Isabelle/HOL A Proof Assistant for Higher-Order Logic /

• Main Authors: Nipkow, Tobias (Author, http://id.loc.gov/vocabulary/relators/aut), Paulson, Lawrence C. (http://id.loc.gov/vocabulary/relators/aut), Wenzel, Markus (http://id.loc.gov/vocabulary/relators/aut)
• Corporate Author: SpringerLink (Online service)
• Format: Electronic eBook
• Language: English
• Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2002.
• Edition: 1st ed. 2002.
• Series: Lecture Notes in Computer Science, 2283
• Subjects: Mathematical logic.; Logic.; Computers.; Artificial intelligence.; Computer logic.; Programming languages (Electronic computers).; Mathematical Logic and Formal Languages.; Theory of Computation.; Artificial Intelligence.; Logics and Meanings of Programs.; Programming Languages, Compilers, Interpreters.

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...

Table of Contents:

• 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.