Tableau基礎理論及應用研究.pdf

1、自動定理證明的擴展之一：自動推理，是人工智能研究的基礎工作。許多重要的人工智能系統(tǒng)，都是以推理系統(tǒng)為其核心部分，所以自動推理的研究，將對人工智能的其它分枝產(chǎn)生深遠的影響，它所提出的推理方法已被應用于人工智能的各個領域。其中的語義tableau方法是由Beth(1959)、Hintikka(1955)提出，而后引入到自動定理證明中。它對于不同的邏輯系統(tǒng)，所使用的tableau規(guī)則是相同的，只是對公式構(gòu)造集進行擴展，使之更接近相應的邏輯系統(tǒng)

2、。由于tableau方法具有較強的通用性和直觀性，從二十世紀六十年代開始，引起了以Smullyan、Fitting為代表的計算機科學家的興趣，同歸結(jié)一樣，被認為是重要的自動推理方法之一。特別是近十年來，引起了更廣泛的關注，許多人在尋求各種各樣的tableau方法。 本文在研究tableau理論的基礎上，主要在命題和一階邏輯中做了以下五個方面的研究： 1.在基本邏輯表示方式的基礎上，重點研究了命題和一階邏輯的范式表示，通過

3、采用析取式重寫等方法，得到了在一階邏輯下，將任意一階公式轉(zhuǎn)化為析取范式的方法，并利用Prolog語言進行了實現(xiàn)。 2.在邏輯語義的基礎上，研究了tableau推理方法(包括命題及一階)，分析原有命題邏輯下實現(xiàn)算法在效率上的不足，對其進行了改進，并進行了有效性和完備性的證明。同樣也針對一階邏輯下的自動推演算法，通過應用與范式轉(zhuǎn)換中相類似的預處理方式進行修改，以簡化后期推演程序，提高效率。 3.在對基本tableau方法擴展