文件名称：论文研究-相干命题逻辑自然推理系统NR的自动证明.pdf
文件大小：662KB
文件格式：PDF
更新时间：2022-08-11 16:01:55
相干命题,自然推理,自动证明,可读证明
给出了相干命题逻辑自然推理系统NR的自动证明算法。首先将待证命题公式A的子公式组成一个初始集合P，对其中的元素采用系统NR的推理规则得到新的命题公式加入P，当得到秩为0的A时命题得证；然后对A的证明树进行整理即得到演绎序列。对系统NR的大部分定理证明取得了良好的效果，算法生成的演绎序列清晰可读，接近手工推理。