歸結(jié)是自動推理中簡潔、可靠且完備的推理規(guī)則。標(biāo)準(zhǔn)矛盾體分離規(guī)則是歸結(jié)原理的一個重要延拓�；诿}邏輯的標(biāo)準(zhǔn)矛盾體分離演繹推理,對標(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)矛盾體中添加子句后另添加文字的策略及子句非擴充性的變化規(guī)律;3)完全標(biāo)準(zhǔn)矛盾體添加子句及相關(guān)文字后,其最小標(biāo)準(zhǔn)矛盾體呈現(xiàn)出的規(guī)律;4)最小標(biāo)準(zhǔn)矛盾體可擴充為完全標(biāo)準(zhǔn)矛盾體。這些結(jié)論使完全標(biāo)準(zhǔn)矛盾體與最小標(biāo)準(zhǔn)矛盾體能通過添加新子句或相關(guān)文字完成互相轉(zhuǎn)換。這一性質(zhì)為標(biāo)準(zhǔn)矛盾體演繹理論進(jìn)一步應(yīng)用于計算機求解提供了一定的理論支撐。 

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

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


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



本文編號：3684722