幫助中心 | 我的帳號 | 關於我們
進階搜尋
car

同類熱銷排行榜

最近瀏覽的商品

電腦科學中的數理邏輯(電腦科學與技術雙色印刷面向新工科專業建設電腦系列教材)

  • 作者：編者:宋麗華//王兆麗//韓敬利//夏青//王元元|責編:楊帆
  • 出版社：清華大學
  • ISBN：9787302713319
  • 出版日期：2026/05/01
  • 裝幀：平裝
  • 頁數：277
人民幣：RMB 69 元      售價：元
放入購物車
加入收藏夾
內容大鋼
    數理邏輯以嚴格的數學方法研究邏輯推理，揭示人類思維的底層規律。作為電腦科學的「微積分」，數理邏輯是程序設計語言、軟體工程、人工智慧等領域的理論基石之一。本書內容理論與應用並重：既涵蓋命題邏輯、一階謂詞邏輯等經典形式系統，系統闡述基本概念與核心理論；又聚焦軟體/硬體驗證的前沿應用，深入介紹程序邏輯、模型檢測技術的演算法實現與工具環境。
    本書適用於電腦類高年級本科生、研究生及工程技術人員。通過研讀本書，讀者可系統提升邏輯思維與形式化建模能力，為從事軟體工程及形式化方法研究奠定專業基礎。
作者介紹
編者:宋麗華//王兆麗//韓敬利//夏青//王元元|責編:楊帆
目錄
第0章  緒論
  0.1  思維、感知的概念化和理性化
  0.2  數理邏輯求助數學——符號化
  0.3  數理邏輯追隨數學——公理化
  0.4  數理邏輯改造數學——形式化
  0.5  數理邏輯與電腦科學
  0.6  本章小結
  0.7  習題
第1章  集合論基礎：概念與運算
  1.1  集合的概念
  1.2  集合運算
  1.3  關係
    1.3.1  關係的基本概念
    1.3.2  關係的基本運算
    1.3.3  關係的特性
    1.3.4  等價關係
    1.3.5  序關係
  1.4  函數
    1.4.1  函數的基本概念及合成運算
    1.4.2  單射、滿射和雙射
    1.4.3  函數的逆
  1.5  本章小結
  1.6  習題
第2章  集合論基礎：歸納
  2.1  集合的歸納定義
  2.2  歸納法
    2.2.1  結構歸納法
    2.2.2  歸納定義及歸納法在電腦科學中的應用
    2.2.3  數學歸納法
  2.3  本章小結
  2.4  習題
第3章  命題演算
  3.1  命題演算基本概念
    3.1.1  命題與聯結詞
    3.1.2  命題公式及其真值
    3.1.3  範式
    3.1.4  聯結詞的擴充與規約
  3.2  命題演算形式系統PC
    3.2.1  PC系統的組成
    3.2.2  PC中的推理
    3.2.3  PC的語義
    3.2.4  關於PC的重要元定理
  3.3  命題演算形式系統ND
  3.4  本章小結
  3.5  習題
第4章  一階謂詞演算
  4.1  一階謂詞演算基本概念
    4.1.1  個體、謂詞和函詞
    4.1.2  變元和常元
    4.1.3  量詞

    4.1.4  謂詞公式
    4.1.5  公式的真值
  4.2  一階謂詞演算形式系統FC
    4.2.1  一階語言
    4.2.2  一階邏輯
  4.3  FC的語義
  4.4  關於FC的重要元定理
    4.4.1  FC的合理性及其他
    4.4.2  FC的完備性及其他
    4.4.3  FC的半可判定性
  4.5  一階謂詞演算自然推理系統FND
  4.6  本章小結
  4.7  習題
第5章  帶等詞的一階謂詞演算
  5.1  等詞公理
  5.2  帶等詞一階系統的語義
  5.3  群論
  5.4  公理化集合論
  5.5  一階算術理論
    5.5.1  一階算術系統組成
    5.5.2  一階算術系統的模型
    5.5.3  皮亞諾公設
  5.6  帶等詞的自然推理系統
  5.7  本章小結
  5.8  習題
第6章  消解原理
  6.1  命題演算的消解原理
    6.1.1  文字、子句和子句集
    6.1.2  消解證明
  6.2  Skolem化
    6.2.1  前束範式
    6.2.2  Skolem標準形
    6.2.3  子句集
  6.3  合一
    6.3.1  代換
    6.3.2  合一基本概念
    6.3.3  合一演算法
  6.4  一階謂詞演算的消解原理
  6.5  消解原理的完備性
    6.5.1  Herbrand結構
    6.5.2  Herbrand定理
    6.5.3  完備性定理的證明
  6.6  本章小結
  6.7  習題
第7章  程序邏輯
  7.1  程序邏輯簡介
  7.2  程序規約
    7.2.1  命令式編程語言WHILE
    7.2.2  斷言與規約
    7.2.3  程序的部分正確性與完全正確性

  7.3  Hoare邏輯系統
    7.3.1  系統組成
    7.3.2  完全正確性的證明
  7.4  Hoare邏輯語義及性質
    7.4.1  WHILE語言語義
    7.4.2  Hoare三元組語義
    7.4.3  關於Hoare邏輯的重要元定理
  7.5  Hoare邏輯的擴展
    7.5.1  對for循環的擴展
    7.5.2  對數組的擴展
  7.6  分離邏輯
    7.6.1  共享可變數據結構
    7.6.2  小堆模型、分離邏輯聯結詞、斷言
    7.6.3  堆操作命令及語義
    7.6.4  公理與推理規則
    7.6.5  鏈表反轉程序的證明
  7.7  自動程序驗證
  7.8  Dafny
    7.8.1  程序與規約：一個例子
    7.8.2  謂詞、假設和定理
    7.8.3  可終止性證明
  7.9  本章小結
  7.10  習題
第8章  模型檢測
  8.1  遷移系統
  8.2  線性時序邏輯LTL
    8.2.1  LTL語法
    8.2.2  LTL語義
    8.2.3  重要的LTL等價式
  8.3  分支時序邏輯CTL
    8.3.1  CTL語法
    8.3.2  CTL語義
    8.3.3  重要的CTL等價式
    8.3.4  CTL與LTL表達能力比較
  8.4  安全性、活性及公平性
  8.5  模型檢測演算法
    8.5.1  LTL模型檢測
    8.5.2  CTL模型檢測
  8.6  Spin
    8.6.1  Promela
    8.6.2  互斥訪問演算法驗證
  8.7  本章小結
  8.8  習題
參考文獻

  • 商品搜索：
  • | 高級搜索
首頁│ 新手上路│ 客服中心│ 關於我們│ 聯絡我們│ Top↑│
Copyrightc 1999~2008 美商天龍國際圖書股份有限公司 臺灣分公司. All rights reserved.
營業地址:臺北市中正區重慶南路一段103號1F 105號1F-2F
讀者服務部電話：02-2381-2033 02-2381-1863　時間：週一-週五 10:00-17:00
　服務信箱：bookuu@69book.com 客戶、意見信箱:cs@69book.com
ICP證：浙B2-20060032