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

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

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