歸結(jié)是自動(dòng)推理中簡(jiǎn)潔、可靠且完備的推理規(guī)則。標(biāo)準(zhǔn)矛盾體分離規(guī)則是歸結(jié)原理的一個(gè)重要延拓�；诿}邏輯的標(biāo)準(zhǔn)矛盾體分離演繹推理,對(duì)標(biāo)準(zhǔn)矛盾體的性質(zhì)進(jìn)行進(jìn)一步研究,提出了兩類特殊標(biāo)準(zhǔn)矛盾體——完全標(biāo)準(zhǔn)矛盾體和最小標(biāo)準(zhǔn)矛盾體,得到了相應(yīng)的性質(zhì)和定理。這些性質(zhì)定理主要描述了:1)各類標(biāo)準(zhǔn)矛盾體的本質(zhì)特征;2)完全標(biāo)準(zhǔn)矛盾體中添加子句后另添加文字的策略及子句非擴(kuò)充性的變化規(guī)律;3)完全標(biāo)準(zhǔn)矛盾體添加子句及相關(guān)文字后,其最小標(biāo)準(zhǔn)矛盾體呈現(xiàn)出的規(guī)律;4)最小標(biāo)準(zhǔn)矛盾體可擴(kuò)充為完全標(biāo)準(zhǔn)矛盾體。這些結(jié)論使完全標(biāo)準(zhǔn)矛盾體與最小標(biāo)準(zhǔn)矛盾體能通過(guò)添加新子句或相關(guān)文字完成互相轉(zhuǎn)換。這一性質(zhì)為標(biāo)準(zhǔn)矛盾體演繹理論進(jìn)一步應(yīng)用于計(jì)算機(jī)求解提供了一定的理論支撐。 

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

【文章目錄】：
1 引言
2 完全標(biāo)準(zhǔn)矛盾體和最小標(biāo)準(zhǔn)矛盾體


【參考文獻(xiàn)】：
期刊論文
[1]多元?jiǎng)討B(tài)演繹在Prover9證明器中的應(yīng)用[J]. 曹鋒,徐揚(yáng),吳貫鋒,鐘建.  計(jì)算機(jī)工程與科學(xué). 2019(09)
[2]多元協(xié)同演繹在一階邏輯ATP中的應(yīng)用[J]. 曹鋒,徐揚(yáng),陳樹(shù)偉,吳貫鋒,常文靜.  西南交通大學(xué)學(xué)報(bào). 2020(02)



本文編號(hào)：3684722