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

• 作者: 曾振柄 郭远华
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 相干逻辑 自动推理 演绎 可读证明 证明树
• 年，卷（期）: 2008,（12）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 105-109
• 页数: 5页
• 分类号: TP181|TP301.6
• 字数: 5210字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2008.12.028

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	曾振柄	华东师范大学软件学院	29	105	6.0	8.0
2	郭远华	华东师范大学软件学院	6	13	2.0	3.0