Tableau基礎(chǔ)理論及應(yīng)用研究.pdf

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

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

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