论文部分内容阅读
在自动定理证明中，我们发现一个卓有成效的证明方法——多余文字参数法．利用这一方法可以简单便捷地证明许多难以证明的各种推理策略中的完备性问题．本文列举了如何应用这一方法来证明自动定理证明中归结原理的完备性、语义归结的完备性、线性归结的完备性以及输入归结和单位归结的等价性问题．事实表明这些原本都是十分棘手的证明问题，由于使用了这一方法而变为十分简单而自然的工作，而且这些不同的完备性问题其证明步骤和过程也几乎是一样的
In the proof of automatic theorems, we found an effective way to prove - redundant text parameter method. This method can be used to easily and easily prove the completeness of many difficult reasoning strategies. This article shows how to apply this method to prove the completeness of the principle of summary, the completeness of the semantic subordination, the completeness of the linear reductions and the equivalence of the input reductions and the unit reductions. The fact that these were all inherently proving problems proved to be very straightforward and natural due to the use of this method and that these different completeness problems proved almost identical in steps and processes