基于有向超圖的命題邏輯合取范式的約簡.pdf

1、在知識表示和自動推理領(lǐng)域，命題邏輯是一種極其重要的形式化語言，其中命題邏輯可滿足性問題是研究最廣泛的核心問題之一，約簡命題邏輯公式是由SAT問題衍生的一個子問題。有向超圖作為普通有向圖的推廣，能夠恰當?shù)乇硎敬笮统W(wǎng)絡(luò)、數(shù)據(jù)庫系統(tǒng)、命題邏輯等研究課題和研究領(lǐng)域中各元素之間的關(guān)系。以有向超圖作為工具是眾多的命題邏輯公式約簡方法中的一種。本文基于命題邏輯和有向超圖的相關(guān)知識、特別是近期的相關(guān)研究工作，主要取得了如下研究結(jié)果:
　　1、針

2、對命題邏輯中一般的合取范式給出了與之一一對應的關(guān)聯(lián)有向超圖的定義，給出一種新的超路徑表示方式，得到了刻畫兩個子句和兩條超邊之間的一些基本關(guān)系的等價命題和性質(zhì)，為進一步利用有向超圖尋找并約簡具有特定的冗余結(jié)構(gòu)的公式奠定了理論基礎(chǔ)。
　　2、通過定義擴展B-圖來表示霍恩公式，得到了其可滿足性的若干結(jié)論及其約簡性質(zhì)，為進一步約簡特定結(jié)構(gòu)的一般公式奠定了基礎(chǔ)。
　　3、將命題邏輯中的冗余對象分為絕對冗余變元、自歸入子句、強歸結(jié)子句這