摘要
给出了相干命题逻辑自然推理系统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.
出处
《计算机应用研究》
CSCD
北大核心
2009年第10期3639-3641,共3页
Application Research of Computers
基金
国家自然科学基金重点资助项目(90718041)
关键词
相干命题
自然推理
自动证明
可读证明
relevance proposition
natural deduction
automated reasoning
readable proof