| 自动定理证明中的一个通用证明法 |
| |
| 引用本文： | 吴茂康,缪淮扣.自动定理证明中的一个通用证明法[J].上海大学学报(自然科学版),1997(3). |
| |
| 作者姓名： | 吴茂康 缪淮扣 |
| |
| 作者单位： | School of Film and Television Art and Technology，Shanghai University |
| |
| 摘 要： | 在自动定理证明中，我们发现一个卓有成效的证明方法——多余文字参数法．利用这一方法可以简单便捷地证明许多难以证明的各种推理策略中的完备性问题．本文列举了如何应用这一方法来证明自动定理证明中归结原理的完备性、语义归结的完备性、线性归结的完备性以及输入归结和单位归结的等价性问题．事实表明这些原本都是十分棘手的证明问题，由于使用了这一方法而变为十分简单而自然的工作，而且这些不同的完备性问题其证明步骤和过程也几乎是一样的
|
| 关 键 词： | 自动定理证明 归结原理 语义归结 线性归结 输入归结 单位归结 |
The Synthesis of Optimum Linear Filter |
| |
| Zhang Pingjia.The Synthesis of Optimum Linear Filter[J].Journal of Shanghai University(Natural Science),1997(3). |
| |
| Authors: | Zhang Pingjia |
| |
| Abstract: | 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. |
| |
| Keywords: | predictive filter Wiener Hopf integral equation time sequence method synthesis |
| 本文献已被 CNKI 等数据库收录！ |
