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

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

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