改進(jìn)γ公式的表推演推理方法研究

摘 要：表推演方法是一種接近于邏輯系統(tǒng)表示的自動(dòng)推理方法，由于其直觀性和通用性，易于計(jì)算機(jī)實(shí)現(xiàn)，因此成為目前最普及的自動(dòng)推理方法之一。在表推演實(shí)現(xiàn)時(shí)，對(duì)γ規(guī)則應(yīng)用次數(shù)的限制至關(guān)重要，限制次數(shù)直接影響表推演的推理效率。給出識(shí)別γ公式方法，提出了含γ公式的表推演推理的改進(jìn)策略，并進(jìn)行了理論證明和系統(tǒng)實(shí)現(xiàn)，該系統(tǒng)與leanTAP軟件包進(jìn)行了對(duì)比實(shí)驗(yàn)。通過對(duì)Pelletier問題的20個(gè)實(shí)例分析，可以看出叩公式不再需要實(shí)例化，大大縮短了表推演的證明過程，減少了搜索空間，提高了推理效率。

關(guān)鍵詞：γ公式；表推演；實(shí)現(xiàn)

中圖法分類號(hào)：TPl81

文獻(xiàn)標(biāo)識(shí)碼：A

文章編號(hào)：1001—3695(2005)01—0041—03