位置:成果数据库 > 期刊 > 期刊详情页
相干命题逻辑自然推理系统NR的自动证明
  • ISSN号:1001-3695
  • 期刊名称:《计算机应用研究》
  • 时间:0
  • 分类:TP181[自动化与计算机技术—控制科学与工程;自动化与计算机技术—控制理论与控制工程]
  • 作者机构:[1]华东师范大学上海市高可信计算重点实验室,上海200062
  • 相关基金:基金项目:国家自然科学基金重点资助项目(90718041)
中文摘要:

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

英文摘要:

This paper presented an automated reasoning algorithm for natural deduction system(NR) ofrelevance propositional logic. Sub-formulas of formula A composed an initial set P, and added the new formulas produced by applying deducing rules of system NR among elements of P to P. Proved proposition A if A was produced and its rank was zero. Then arranged the reasoning tree of A and achieved the deduction sequence. This algorithm is effective for most theorems in system NR. The deduction sequences created by the algorithm are readable and similar to human prooves.

同期刊论文项目
同项目期刊论文
期刊信息
  • 《计算机应用研究》
  • 北大核心期刊(2011版)
  • 主管单位:四川省科学技术厅
  • 主办单位:四川省计算机研究院
  • 主编:刘营
  • 地址:成都市成科西路3号
  • 邮编:610041
  • 邮箱:arocmag@163.com
  • 电话:028-85210177 85249567
  • 国际标准刊号:ISSN:1001-3695
  • 国内统一刊号:ISSN:51-1196/TP
  • 邮发代号:62-68
  • 获奖情况:
  • 第二届国家期刊奖百种重点科技期刊,国内计算技术类重点核心期刊,国内外著名数据库收录期刊
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,波兰哥白尼索引,英国科学文摘数据库,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊(2004版),中国北大核心期刊(2008版),中国北大核心期刊(2011版),中国北大核心期刊(2014版),中国北大核心期刊(2000版)
  • 被引量:60049