相干命题逻辑系统R的一种演绎生成算法

摘要：

本文提出了相干命题逻辑系统R的一种演绎生成算法--试探法。该算法采用后向推理法,依据推理规则将待证命题逐步分解成子命题并构造一棵证明树,对系统R中的定理证明取得了较好的效果.

关键词： 相干逻辑 自动推理 可读证明 证明树 演绎算法 试探法 推理规则

作者: 郭远华 曾振柄

作者单位: 华东师范大学软件学院,上海,200062

会议类型: 国内会议

会议名称: 2008年全国理论计算机科学学术年会

会议地点: 西安

会议语种:中文

页码: 105-109

在线出版日期: 2008-09-19（万方平台首次上网日期，不代表论文的发表时间）