基于归结方法的定理机器证明

本课题组自1994年1月 开始执行本课题《基于归结方法的定理机器证明》以来，围绕归结推理方法，按照课题的研究计划和研究内容，深入细致地开展了研究工作，取得了一批重要的研究成果。发表学术论文26篇，其中中国科学1篇，计算机学报9篇，软件学报6篇，吉大学报3篇，计算机科学3篇，国际国内会议6篇；另有若干成果待发表；出版学术专著2本。获吉林省教委科技进步一等奖一次（1995年）。在一下几方面取得成果：1、经典逻辑基于归结方法的定理机器证明；2、布尔算子模糊逻辑及其归结形式推理；3、模态逻辑的归结推理方法；4、非单调逻辑的形式推理；5、约束可满足问题求解方法、溯因推时及其应用。