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

Automated reasoning for natural deduction system NR of relevance propositional logic

作　　者：郭远华[1] 曾振柄[1] 

机构地区：[1]华东师范大学上海市高可信计算重点实验室,上海200062

出　　处：《计算机应用研究》2009年第10期3639-3641,共3页Application Research of Computers

基　　金：国家自然科学基金重点资助项目(90718041)

摘　　要：给出了相干命题逻辑自然推理系统NR的自动证明算法。首先将待证命题公式A的子公式组成一个初始集合P,对其中的元素采用系统NR的推理规则得到新的命题公式加入P,当得到秩为0的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.

关 键 词：相干命题 自然推理 自动证明 可读证明 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]