面向計(jì)算機(jī)科學(xué)的數(shù)理邏輯系統(tǒng)建模與推理

數(shù)理邏輯是計(jì)算機(jī)科學(xué)的基礎(chǔ)之一，在模型與系統(tǒng)的規(guī)約與驗(yàn)證等方面有著廣泛的應(yīng)用。隨著當(dāng)今軟硬件產(chǎn)品日趨復(fù)雜，數(shù)理邏輯已經(jīng)成為越來(lái)越多設(shè)計(jì)開(kāi)發(fā)人員的日常工具。

本書適合作為高等院校計(jì)算機(jī)及相關(guān)專業(yè)的數(shù)理邏輯/形式化方法課程教材，涵蓋了命題邏輯，謂詞邏輯、模態(tài)邏輯與 Agent、二元決策圖、模型檢查和程序驗(yàn)證等內(nèi)容。與傳統(tǒng)數(shù)理邏輯教科書相比，它的主要特色就是緊緊圍繞軟硬件規(guī)約和驗(yàn)證這一主題，反映了計(jì)算機(jī)科學(xué)中數(shù)理邏輯的新發(fā)展和實(shí)際需要。第2版新增了可滿足性算法，緊致性理論和Lowenhenm-Skolem定理，并介紹了Alloy語(yǔ)言和Nusmv工具。

本書自出版以來(lái)受到廣泛好評(píng)，已經(jīng)被包括美國(guó)普林斯頓大學(xué)、卡內(nèi)基-梅隆大學(xué)、英國(guó)劍橋大學(xué)、德國(guó)漢堡大學(xué)、加拿大多倫多大學(xué)、荷蘭 Vrije大學(xué)，印度理工學(xué)院在內(nèi)的多個(gè)國(guó)家?guī)资咝２杉{為教材。