摘要
在自动定理证明中，我们发现一个卓有成效的证明方法——多余文字参数法．利用这一方法可以简单便捷地证明许多难以证明的各种推理策略中的完备性问题．本文列举了如何应用这一方法来证明自动定理证明中归结原理的完备性、语义归结的完备性、线性归结的完备性以及输入归结和单位归结的等价性问题．事实表明这些原本都是十分棘手的证明问题，由于使用了这一方法而变为十分简单而自然的工作。
This paper advances a time sequence method for solving the Wiener Hopf integral equation,and uses this method to synthesize the optimum linear filter. This method can be not only used directly in interrelated functions given by graphs or figure columns, but also adopted in avoiding difficulties to solve realizable problems.
出处
《上海大学学报（自然科学版）》
CAS
CSCD
1997年第3期283-288,共6页
Journal of Shanghai University:Natural Science Edition
基金
863高科技项目
关键词
自动定理证明
归结原理
语义归结
计算机证明
predictive filter
Wiener Hopf integral equation
time sequence method
synthesis
