邏輯公式的可滿足性問題是計算機科學和人工智慧中的著名問題.本書前三章主要介紹經典的命題邏輯和一階謂詞邏輯公式以及模態邏輯公式的可滿足性判定算法,也介紹了有關的軟體工具.第四章則介紹它們在離散數學研究、軟體和硬體的形式驗證與測試等方面的套用.
基本介紹
- 作者:張健
- ISBN:9787030083647
- 定價:18.0
- 出版社:科學出版社
- 出版時間:2000-10-01
內容介紹,作品目錄,
內容介紹
本書可供從事計算機科學和人工智慧研究的有關人員閱讀,也可供高等院校計算機專業的本科生和研究生參考.
作品目錄
序
前言
引言
第一章命題邏輯
§1.1命題邏輯簡介
§1.2可滿足性問題
§1.2.1合取範式的可滿足性問題
§1.2.2約束滿足問題
§1.3Davis??Putnam算法
§1.3.1DP算法
§1.3.2分支策略
§1.3.3其他提高效率的手段
§1.4局部搜尋法
§1.5有序二叉判定圖
§1.6語義表和Stalmarck方法
§1.6.1語義表
§1.6.
前言
引言
第一章命題邏輯
§1.1命題邏輯簡介
§1.2可滿足性問題
§1.2.1合取範式的可滿足性問題
§1.2.2約束滿足問題
§1.3Davis??Putnam算法
§1.3.1DP算法
§1.3.2分支策略
§1.3.3其他提高效率的手段
§1.4局部搜尋法
§1.5有序二叉判定圖
§1.6語義表和Stalmarck方法
§1.6.1語義表
§1.6.