邏輯定理的機器證明是人工智能領(lǐng)域人們最早從事研究的課題。本書從邏輯定理的人工證明和機器證明兩方面來展現(xiàn)邏輯定理證明的藝術(shù)，而機器證明又從定理的自動證明和計算機輔助證明兩個方面來展現(xiàn)。本書首先用作者構(gòu)造的命題演算系統(tǒng)FPC和狹謂詞演算系統(tǒng)FQC完成常用邏輯定理的人工證明(一種自然推理證明)。其次，用邏輯定理的機器證明工具TPG(Tree Proof Generator)實現(xiàn)邏輯定理的自動證明(一種樹證明)。最后，用交互式定理機器證明工具Fitch實現(xiàn)了邏輯定理的計算機證明(一種自然推理證明)。

更多科學(xué)出版社服務(wù)，請掃碼獲取。