1、知識(shí)表示、知識(shí)推理和知識(shí)應(yīng)用是人工智能的核心問題。目前，基于非經(jīng)典邏輯的自動(dòng)推理系統(tǒng)由于它加速了人工智能的發(fā)展而越來越引起人們的廣泛重視。為了處理不同信息的推理，人們提出并發(fā)展了多種數(shù)學(xué)理論、方法和工具。如歸結(jié)原理、經(jīng)典邏輯、模糊邏輯、格值邏輯、Rou曲邏輯以及Petri網(wǎng)理論等，這些理論和方法為自動(dòng)推理提供了強(qiáng)有力的支持。本文在自動(dòng)推理領(lǐng)域中，進(jìn)一步發(fā)展了現(xiàn)有的理論和方法，研究了基于Petri網(wǎng)模型的歸結(jié)自動(dòng)推理系統(tǒng)，并取得了如下主要

2、研究成果： 1.給出了子句集的矩陣表示形式，根據(jù)單文字規(guī)則與純文字規(guī)則，討論了矩陣的化簡策略，并定義了子句集矩陣的初等變換，研究了變換的性質(zhì)。根據(jù)Petri網(wǎng)中T-不變量推理判定法的思想，并結(jié)合輸入歸結(jié)、單元?dú)w結(jié)以及支撐歸結(jié)，提出了多種矩陣歸結(jié)的推理方法，證明了推理算法的完備性。 2.給出了基于Horn基子句集、一般基子句集和一階Horn子句集的Petri網(wǎng)模型。根據(jù)Petri網(wǎng)中標(biāo)識(shí)的流動(dòng)規(guī)則，結(jié)合歸結(jié)原理，給出了基于

3、Petri網(wǎng)模型的刪除歸結(jié)推理算法，證明了算法的完備性。并將刪除歸結(jié)推理算法與T一不變量推理算法進(jìn)行了比較，得到重要的結(jié)論：T一不變量推理算法簡單，但使用范圍有限，推理過程不直觀；刪除歸結(jié)推理算法具有普適性，’有直觀的推理過程，推理具有高效性，結(jié)構(gòu)表示具有簡潔性等優(yōu)點(diǎn)。這些研究結(jié)果為基于Petri網(wǎng)模型的歸結(jié)自動(dòng)推理提供了簡單有效的推理方法。 3.提出了算子命題邏輯系統(tǒng)，討論了算子命題邏輯系統(tǒng)中的λ．恒假、λ．歸結(jié)以及λ．歸結(jié)演

4、繹等的邏輯性質(zhì)，證明了λ．歸結(jié)演繹的完備性。討論了命題子句的極簡規(guī)則型范式，給出了算子命題公式的Petri網(wǎng)模型，提出了算子命題邏輯系統(tǒng)中的兩種歸結(jié)推理算法一T一不變量推理算法與刪除歸結(jié)推理算法，證明了推理算法的完備性。 4.針對一類推理模型，提出了一種更一般的算子邏輯系統(tǒng)即算子模糊邏輯系統(tǒng)，討論了算子模糊邏輯系統(tǒng)中的λ．歸結(jié)以及λ．歸結(jié)演繹的邏輯性質(zhì)，給出了算子模糊邏輯系統(tǒng)中的提升引理，由此證明了λ．歸結(jié)演繹的完備性。討論了算

5、子模糊邏輯系統(tǒng)中算子模糊子句的Horn型及一般型兩種Petri網(wǎng)模型，給出了基于表示模型的T-不變量推理算法和刪除歸結(jié)推理算法，證明了推理算法的完備性。所有這些表示方法和推理算法，為模糊邏輯系統(tǒng)的推理提供了新的方法與思路。 5．為了進(jìn)一步研究非經(jīng)典邏輯系統(tǒng)的自動(dòng)推理，特別是較直觀的推理形式，給出了格值命題邏輯系統(tǒng)LP(X)中公式的Petri網(wǎng)模型及基于Petri網(wǎng)模型的歸結(jié)推理算法。討論了格值命題邏輯系統(tǒng)LP(X)中公式的規(guī)則型

6、范式，定義了極簡規(guī)則型子句的MP歸結(jié)以及(A，口)．歸結(jié)演繹，證明了歸結(jié)演繹的可靠性與弱完備性。討論了極簡規(guī)則型子句集的Petri網(wǎng)模型以及任意公式的Petri網(wǎng)模型。詳細(xì)給出了四值非鏈格值命題邏輯系統(tǒng)LP4(X)的Petri網(wǎng)推理模型及推理算法，進(jìn)一步給出了格值命題邏輯系統(tǒng)LP(X)中公式的Petri網(wǎng)推理模型以及基于Petri網(wǎng)模型的T-不變量推理算法和可達(dá)性推理算法，證明了推理算法的完備性，得到了有意義的結(jié)論，從而為研究格值命題邏