改進γ公式的表推演推理方法研究

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

關鍵詞：γ公式；表推演；實現

中圖法分類號：TPl81

文獻標識碼：A

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