Automated reasoning for natural deduction system NR of relevance propositional logic
相干命题逻辑自然推理系统NR的自动证明*

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.