自动定量证明中的一个通用证明法 |
| |
引用本文: | 吴茂康,缪淮扣.自动定量证明中的一个通用证明法[J].上海大学学报(自然科学版),1997,3(3):283-288. |
| |
作者姓名: | 吴茂康 缪淮扣 |
| |
摘 要: | 在自动定理证明中,我们发现一个卓有成效的证明方法-多余文字参数法。利用这一方法可以简单便捷地证明许多难以证明的各种推理策略中的完备性问题。本文列举了如何应用这一方法来证明自动定理证明中归结原理的完备性,语义归结完备性,线性归结的完备性以及输入归结和单位归结的等价性问题。
|
关 键 词: | 自动定理证明 归结原理 语义归结 计算机证明 |
本文献已被 维普 等数据库收录! |
|