基於歸結方法的定理機器證明

《基於歸結方法的定理機器證明》是依託吉林大學，由劉敘華擔任項目負責人的面上項目。

基本介紹

• 中文名：基於歸結方法的定理機器證明
• 項目類別：面上項目
• 項目負責人：劉敘華
• 依託單位：吉林大學
• 批准號：69373004
• 申請代碼：F0201
• 負責人職稱：教授
• 研究期限：1994-01-01 至 1996-12-31
• 支持經費：6（萬元）

項目摘要

本課題組自1994年1月 開始執行本課題《基於歸結方法的定理機器證明》以來，圍繞歸結推理方法，按照課題的研究計畫和研究內容，深入細緻地開展了研究工作，取得了一批重要的研究成果。發表學術論文26篇，其中中國科學1篇，計算機學報9篇，軟體學報6篇，吉大學報3篇，計算機科學3篇，國際國內會議6篇；另有若干成果待發表；出版學術專著2本。獲吉林省教委科技進步一等獎一次（1995年）。在一下幾方面取得成果：1、經典邏輯基於歸結方法的定理機器證明；2、布爾運算元模糊邏輯及其歸結形式推理；3、模態邏輯的歸結推理方法；4、非單調邏輯的形式推理；5、約束可滿足問題求解方法、溯因推時及其套用。