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

定　價(jià)：￥45.00

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

購(gòu)買這本書可以去

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

內(nèi)容簡(jiǎn)介

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

作者簡(jiǎn)介

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

圖書目錄

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