摘要
本文证明了一阶定理证明的余式方法（见文献［５］）对于线性策略是完备的，而对于语义策略和锁策略，在命题演算中是完备的，在一阶谓词演算中，对于一种较弱形式的语义策略和锁策略，是完备的．
The remainder method in first-order theorem proving is complete for linear strategy. For semantic strategy and lock strategy,it is complete in propositional calculus. In predicate calculus, it is complete for semantic strategy and lock strategy of a weak form.
出处
《计算机学报》
EI
CSCD
北大核心
1997年第2期174-178,共5页
Chinese Journal of Computers
基金
国家博士后科学基金
攀登计划项目
"机器证明及其应用"基金
关键词
线性策略
余式法
机器证明
First-order polynomials, linear remainder method, semantic remainder method, lock remainder method.
