面向計算機科學的數理邏輯-系統建模與推理 (原書第2版) 9787111770688 邁克爾.休斯 馬克.萊恩

*書籍均為代購，我們向大陸付款發訂後即無法取消，為避免造成不必要的損失，
下訂前請慎重考慮！下訂前請慎重考慮！謝謝。
*完成訂單後正常情形下約兩周可抵台。
*本賣場提供之資訊僅供參考，以到貨標的為正確資訊。
印行年月：202502*若逾兩年請先於客服中心或Line洽詢存貨情況，謝謝。
台灣(台北市)在地出版社，每筆交易均開具統一發票，祝您中獎最高1000萬元。
書名：面向計算機科學的數理邏輯-系統建模與推理 (原書第2版)
ISBN：9787111770688
出版社：機械工業
著編譯者：邁克爾.休斯 馬克.萊恩
頁數：277
所在地：中國大陸 *此為代購商品
書號：1716981
可大量預訂，請先連絡。

【台灣高等教育出版社簡體書】 面向計算機科學的數理邏輯-系統建模與推理 (原書第2版) 787111770688 邁克爾.休斯 馬克.萊恩

內容簡介

數理邏輯是計算機科學的基礎之一，在模型與系統的規範與驗證等方面有著廣泛的應用。隨著當今軟硬體產品（電路、程序和通信協議等）日趨複雜，數理邏輯已經成為設計開發人員的日常工具。 作為計算機及其相關專業的數理邏輯課程教材，本書自出版以來受到了廣泛的好評，世界許多著名大學（比如美國普林斯頓大學、卡內基?梅隆大學、英國劍橋大學、德國漢堡大學、加拿大多倫多大學、荷蘭Vrije大學、印度理工學院）都採用本書作為教材。 全書涵蓋了命題邏輯、謂詞邏輯、模態邏輯與代理、二叉判定圖、模型檢測和程序驗證等內容。主要特色就是緊緊圍繞軟硬體規約和驗證這一主題，反映計算機科學中數理邏輯的發展和實際需要。第2版新增了可滿足性（SAT）算法、緊緻性理論和L?wenheim-Skolem定理，並介紹了Alloy語言和NuSMV工具。 本書適合作為高等院校計算機及相關專業的數理邏輯/形式化方法課程的教材，也可供相關研究人員和專業人士參考。

作者簡介

邁克爾·休斯（Michael Huth）現任紐倫堡科技大學（UTN）創始校長。在加入UTN之前，休斯教授曾在倫敦帝國理工學院工作，歷任計算機科學教授、計算機系主任，並將繼續擔任客座教授。在研究和教學方面，他目前的研究重點是人工智能和網絡安全領域的前瞻性課題。

目錄

譯者序
第1版序
第2版前言
致謝
第1章 命題邏輯
1 1 判斷語句
1 2 自然演繹
1 2 1 自然演繹規則
1 2 2 派生規則
1 2 3 自然演繹總結
1 2 4 邏輯等價
1 2 5 側記：反證法
1 3 作為形式語言的命題邏輯
1 4 1 邏輯連接詞的含義
1 4 2 數學歸納法
1 4 3 命題邏輯的合理性
1 4 4 命題邏輯的完備性
1 5 範式
1 5 1 語義等價、滿足性和有效性
1 5 2 合取範式和有效性
1 5 3 霍恩子句和可滿足性
1 6 SAT求解機
1 6 1 線性求解機
1 6 2 三次求解機
1 7 習題
1 8 文獻註釋
第2章 謂詞邏輯
2 1 我們需要更豐富的語言
2 2 作為形式語言的謂詞邏輯
2 2 1 項
2 2 2 公式
2 2 3 自由變數和約束變數
2 2 4 代換
2 3 謂詞邏輯的證明論
2 3 1 自然演繹規則
2 3 2 量詞的等價
2 4 謂詞邏輯的語義
2 4 1 模型
2 4 2 語義推導
2 4 3 相等的語義
2 5 謂詞邏輯的不可判定性
2 6 謂詞邏輯的表達能力
2 6 1 存在式二階邏輯
2 6 2 全稱式二階邏輯
2 7 軟體的微觀模型
2 7 1 狀態機
2 7 2 Alma重現
2 7 3 軟體的微模型
2 8 習題
2 9 文獻註釋
第3章 通過模型檢測進行驗證
3 1 驗證的動機
3 2 線性時態邏輯
3 2 1 LTL的語法
3 2 2 LTL的語義
3 2 3 規範的實際模式
3 2 4 LTL公式之間的重要等價
3 2 5 LTL的適當連接詞集
3 3 模型檢測：系統、工具和性質
3 3 1 例：互斥
3 3 2 NuSMV模型檢測器
3 3 3 運行NuSMV
3 3 4 重濕互斥
3 3 5 擺渡者難題
3 3 6 交錯位協議
3 4 分支時間邏輯
3 4 1 CTL的語法
3 4 2 計算樹邏輯的語義
3 4 3 規範的實際模式
3 4 4 CTL公式間的重要等價
3 4 5 CTL連接詞的適當集
3 5 CTL與LTL和CTL的表達能力
3 5 1 CTL中時態公式的布爾組合
3 5 2 LTL中的過去運算元
3 6 模型檢測算法
3 6 1 CTL模型檢測算法
3 6 2 具有公平性的CTL模型檢測
3 6 3 LTL模型檢測算法
3 7 CTL的不動點特徵
3 7 1 單調函數
3 7 2 SAT的正確性
3 7 3 SAT的正確性
3 8 習題
3 9 文獻註釋
第4章 程序驗證
4 1 為什麼要規範和驗證編程
4 2 軟體驗證的一種框架
4 2 1 一種核心程序設計語言
4 2 2 霍爾三元組
4 2 3 部分正確性和完全正確性
4 2 4 程序變數和邏輯變數
4 3 部分正確性的證明演算
4 3 1 證明規則
4 3 2 證明布景
4 3 3 案例研究：最小和截段
4 4 完全正確性的證明演算
4 5 合同編程
4 6 習題
4 7 文獻註釋
第5章 模態邏輯與代理
5 1 真值的模式
5 2 基本模態邏輯
5 2 1 語法
5 2 2 語義
5 3 邏輯工程
5 3 1 有效公式儲備
5 3 2 可達關係的重要性質
5 3 3 對應理論
5 3 4 一些模態邏輯
5 4 自然演繹
5 5 多代理系統中的知識推理
5 5 1 一些例子
5 5 2 模態邏輯KT45
5 5 3 KT45的自然演繹
5 5 4 例子的形式化
5 6 習題
5 7 文獻註釋
第6章 二叉判定圖
6 1 布爾函數的表示
6 1 1 命題公式和真值表
6 1 2 二叉判定圖
6 1 3 有序BDD
6 2 簡約OBDD的算法
6 2 1 算法reduce
6 2 2 算法apply
6 2 3 算法restrict
6 2 4 算法exists
6 2 5 OBDD的評價
6 3 符號模型檢測
6 3 1 表示狀態集合的子集
6 3 2 表示遷移關係
6 3 3 實現函數preE和preA
6 3 4 綜合OBDD
6 4 關係μ演算
6 4 1 語法和語義
6 4 2 對CTL模型及規範說明的編碼
6 5 習題
6 6 文獻註釋
參考文獻
詳細資料或其他書籍請至台灣高等教育出版社查詢，查後請於客服中心或Line或本社留言板留言，我們即儘速上架。

大陸簡體正版圖書，訂購後正常情形下約兩周可抵台。