《基於tableau的非經典邏輯經典化的自動定理證明研究》是依託蘇州大學，由劉全擔任項目負責人的面上項目。
基本介紹
- 中文名：基於tableau的非經典邏輯經典化的自動定理證明研究
- 項目類別：面上項目
- 項目負責人：劉全
- 依託單位：蘇州大學
- 批准號：60873116
- 申請代碼：F0201
- 負責人職稱：教授
- 研究期限：2009-01-01 至 2011-12-31
- 支持經費：35（萬元）
項目摘要
自動定理證明是涉及人類智慧型問題的重要研究課題之一，對人工智慧的研究具有重要的影響和推動作用。本項目針對非經典邏輯缺乏有效的自動定理證明過程的問題，提出將非經典邏輯通過轉化，用經典邏輯進行tableau自動定理證明的方法。該方法在經典邏輯的基礎上，將邏輯強化學習、歸納邏輯程式設計、布爾剪枝、等式合一、等價翻譯等方法套用於非經典邏輯中，使得複雜的非經典邏輯定理可以在經典層面上來證明。一方面，一些提高經典邏輯證明效率的方法，可以套用到非經典邏輯中；另一方面，一些經典邏輯自動定理證明系統只要稍加改動就很容易擴展成為非經典邏輯系統。本項目的研究成果將在符號自動定理證明理論和方法上有所貢獻，可以有效地擴大tableau推理的適用範圍，在時間和空間上提高證明效率，更大程度地減少tableau擴展的盲目性和不確定性。
