%0 Journal Article
%T Automated reasoning for natural deduction system NR of relevance propositional logic<br>相干命题逻辑自然推理系统NR的自动证明*
%A GUO Yuan-hu
%A ZENG Zhen-bing
%A <br>郭远华
%A 曾振柄
%J 计算机应用研究
%D 2009
%I 
%X This paper presented an automated reasoning algorithm for natural deduction system(NR)of relevance propositio-nal 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.
%K relevance proposition
%K natural deduction
%K automated reasoning
%K readable proof<br>相干命题
%K 自然推理
%K 自动证明
%K 可读证明
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=A9D9BE08CDC44144BE8B5685705D3AED&aid=ED33B380E6C8D9D9766B1F0E26108436&yid=DE12191FBD62783C&vid=96C778EE049EE47D&iid=F3090AE9B60B7ED1&sid=D4F776EAD553D4D6&eid=80C30AAF683A42F9&journal_id=1001-3695&journal_name=计算机应用研究&referenced_num=0&reference_num=7