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