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

• Κύριοι συγγραφείς: Nipkow, Tobias (Συγγραφέας, 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)
• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2002.
• Έκδοση: 1st ed. 2002.
• Σειρά: Lecture Notes in Computer Science, 2283
• Θέματα: 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...