相干命题逻辑自然推理系统NR的自动证明

• 作者: 曾振柄 郭远华
• 来源期刊: 计算机应用研究
• 关键词: 相干命题 自然推理 自动证明 可读证明
• 年，卷（期）: 2009,（10）
• 所属期刊栏目: 算法研究探讨
• 页码范围: 3639-3641
• 页数: 3页
• 分类号: TP181
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2009.10.010

摘要

给出了相干命题逻辑自然推理系统NR的自动证明算法.首先将待证命题公式A的子公式组成一个初始集合P,对其中的元素采用系统NR的推理规则得到新的命题公式加入P,当得到秩为0的A时命题得证;然后对A的证明树进行整理即得到演绎序列.对系统NR的大部分定理证明取得了良好的效果,算法生成的演绎序列清晰可读,接近手工推理.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	曾振柄	华东师范大学上海市高可信计算重点实验室	29	105	6.0	8.0
2	郭远华	华东师范大学上海市高可信计算重点实验室	6	13	2.0	3.0