高階邏輯輔助證明系統(tǒng)

定　價：￥45.00

作　者：	（德）托比亞斯·尼普科夫，（英）勞倫斯·鮑爾森，（德）瑪爾庫斯·溫澤爾著，陳光喜，劉卓軍譯
出版社：	北京理工大學(xué)出版社
叢編項：
標(biāo)　簽：	工學(xué) 教材研究生/本科/專科教材

購買這本書可以去

ISBN：	9787564077631	出版時間：	2013-05-01	包裝：	精裝
開本：	32開	頁數(shù)：	253	字?jǐn)?shù)：

內(nèi)容簡介

　　《高階邏輯輔助證明系統(tǒng)》是在高階邏輯中使用Isabelle輔助證明系統(tǒng)進(jìn)行交互式證明的導(dǎo)論，適用于Isabelle系統(tǒng)的潛在使用者，自成體系，分為三部分：第一部分是基本技巧：介紹在高階邏輯中如何進(jìn)行函數(shù)式程序建模，提供了表（1ist）和自然數(shù)的簡單證明實例。大多數(shù)證明只要兩步完成：對所選變量進(jìn)行歸納以及使用自動策略（auto）。當(dāng)然，這些粗淺的例子仍然涵蓋了嵌套遞歸和交叉遞歸等技術(shù)。第二部分是邏輯與集合：介紹大量可供選擇使用的低級證明策略。《高階邏輯輔助證明系統(tǒng)》描述了Isabelle／HOL如何處理集合、函數(shù)、關(guān)系以及如何實現(xiàn)遞歸定義集合，包括模型檢驗理論和經(jīng)典教科書中關(guān)于形式語言的案例。第三部分是高級話題：包括實數(shù)、記錄、重載技術(shù)等主題。《高階邏輯輔助證明系統(tǒng)》也討論了歸納法和遞歸方法的高級技巧，還專門給出一章來介紹安全協(xié)議的形式化驗證。

作者簡介

暫缺《高階邏輯輔助證明系統(tǒng)》作者簡介

圖書目錄

第一部分  基本技巧
第一章  基礎(chǔ)
1.1  引言
1.2  theory（理論）
1.3  類型，項和公式
1.4  變元
1.5  交互與界面
1.6  啟動
第二章  HOL中的函數(shù)編程
第三章  高級函數(shù)式編程
第四章  theory的表示
第二部分  邏輯與集合
第五章  游戲規(guī)則
第六章  集合、函數(shù)和關(guān)系
第七章  集合遞歸定義
第八章  高級types
第九章  高級化簡與歸納
第十章  案例學(xué)習(xí)：驗證安全協(xié)議
附錄
參考文獻(xiàn)
譯后記一