高階邏輯輔助證明系統

本書分基本技巧、邏輯與集合、高級材料三部分，內容包括：基礎、HOL中的函式編程、高級函式式編程、遊戲規則、集合遞歸定義等。

基本介紹

• 書名：高階邏輯輔助證明系統
• 作者：托比亞斯·尼普科夫 勞倫斯·鮑爾森
• 出版日期：2013年5月1日
• 語種：簡體中文
• 外文名：A Proof Assistant for Higher-Order Logic
• 出版社：北京理工大學出版社
• 頁數：253頁
• 開本：32

基本介紹

內容簡介

托比亞斯·尼普科夫、(英)勞倫斯·鮑爾森、瑪爾庫斯·溫澤爾編著的《高階邏輯輔助證明系統(精)》是在高階邏輯中使用Isabelle輔助證明系統進行互動式證明的導論，適用於Isabelle系統的潛在使用者，自成體系，分為三部分：第一部分是基本技巧：介紹在高階邏輯中如何進行函式式程式建模，提供了表(1ist)和自然數的簡單證明實例。大多數證明只要兩步完成：對所選變數進行歸納以及使用自動策略(auto)。當然，這些粗淺的例子仍然涵蓋了嵌套遞歸和交叉遞歸等技術。第二部分是邏輯與集合：介紹大量可供選擇使用的低級證明策略。本部分描述了Isabelle/HOL如何處理集合、函式、關係以及如何實現遞歸定義集合，包括模型檢驗理論和經典教科書中關於形式語言的案例。第三部分是高級話題：包括實數、記錄、重載技術等主題。本部分也討論了歸納法和遞歸方法的高級技巧，還專門給出一章來介紹安全協定的形式化驗證。

作者簡介

作者:(德)托比亞斯·尼普科夫、(英)勞倫斯·鮑爾森、(德)瑪爾庫斯·溫澤爾 譯者:陳光喜、劉卓軍

圖書目錄

第一部分 基本技巧
第一章 基礎
1．1 引言
1．2 theory(理論)
1．3 類型，項和公式
1．4 變元
1．5 互動與界面
1．6 啟動
第二章 HOL中的函式編程
第三章 高級函式式編程
第四章 theory的表示
第二部分 邏輯與集合
第五章 遊戲規則
第六章 集合、函式和關係
第七章 集合遞歸定義
第八章 高級types
第九章 高級化簡與歸納
第十章 案例學習：驗證安全協定
附錄
參考文獻
譯後記一