本文針對(duì)命題演算形式系統(tǒng),在機(jī)器輔助定理證明系統(tǒng)Isabelle/HOL中為其建立邏輯模型,并分別形式化驗(yàn)證了PC和ND的主要性質(zhì),以及完備性定理的證明。通過(guò)對(duì)PC和ND的分析和驗(yàn)證表明,采用機(jī)器輔助定理證明系統(tǒng),對(duì)以數(shù)理邏輯為平臺(tái)的各種形式系統(tǒng)進(jìn)行嚴(yán)格的分析和證明是可行的。 

【文章來(lái)源】：計(jì)算機(jī)工程與科學(xué). 2008,(10)北大核心

【文章頁(yè)數(shù)】：3 頁(yè)

【文章目錄】：
1 引言
2 命題演算形式系統(tǒng)PC
    2.1 PC的基本構(gòu)成
    2.2 系統(tǒng)內(nèi)的推理
        2.2.1 命題公式的真值
        2.2.2 證明和演繹
3 完備性定理的證明
4 命題演算形式系統(tǒng)ND
5 結(jié)束語(yǔ)



本文編號(hào)：3235003