使用广义奇-超位Ⅱ的一阶定理证明

导出

摘要证明了使用奇-超位Ⅱ的证明系统是不完备的,造成这种不完备性的原因是忽略了幂等规则的作用.通过定义一阶多项式与零的超位,适当地拓广了奇-超位Ⅱ的定义,给出了一个使用这种拓广了的奇-超位Ⅱ的完备的证明系统.此外,这一证明系统也是余式方法的改进,它的完备性实质上也说明了使用语义策略的余式方法是完备的.

作者吴尽昭刘卓军

机构地区北京大学数学系中国科学院系统科学研究所

出处《中国科学（E辑）》 CSCD 1996年第5期442-449,共8页 Science in China(Series E)

基金国家"攀登计划"基金国家教委博士后科学基金资助项目

关键词定理证明一阶多项式奇-超位Ⅱ 广义

分类号 O174.14 [理学—基础数学] TP391.75 [自动化与计算机技术—计算机应用技术]

引文网络
相关文献

参考文献7

1Wu J Z，Proc of the 1st ASCM，1995年
2Liu X H，J Comput & Technol，1994年，9卷，2期，160页
3Zhang H，J Symbolic Computation，1994年，17卷，189页
4刘叙华，定理机器证明，1987年
5吴文俊，几何定理机器证明的基本原理，1984年
6王湘浩，计算机学报，1982年，5卷，2期，81页
7Chang C L，Symbolic Logic and Mechanical Theorem Proving，1973年

1吴尽昭,刘卓军.一阶谓词演算定理机器证明的余式方法[J].计算机学报,1996,19(10):728-734. 被引量：7
2吴尽昭,刘卓军.余式方法中的线性策略以及语义策略和锁策略[J].计算机学报,1997,20(2):174-178.
3张孝令,刘福昇,蒋金凤.一阶多项式动态模型及贝叶斯预测[J].数学的实践与认识,1991,21(2):69-77. 被引量：7
4陈壮奕.CRC校验的C语言实现[J].计算技术与自动化,2001(z1):257-261. 被引量：1
5enoch.XFX教你玩高清——终极解码菜鸟教程[J].微型计算机,2008,28(7):64-64.
6陈勇,刘群锋,黄仁泰.支持向量机一阶多项式光滑函数的唯一性分析[J].信息与电脑（理论版）,2009(12):16-17.
7伍忠东,高新波,谢维信.基于核方法的模糊聚类算法[J].西安电子科技大学学报,2004,31(4):533-537. 被引量：75
8张子蓬,王淑青.解决DS1820通讯误码问题的方法[J].电测与仪表,2001,38(2):23-25.
9曾楚芝.大学英语词汇教学中的认知对比研究[J].文教资料,2014(14):185-186. 被引量：1
10肖海青,刘高嵩,尹美林.一种新的基于CRC的文本内容认证方法[J].哈尔滨商业大学学报（自然科学版）,2006,22(4):84-87.

中国科学（E辑）

1996年第5期

浏览历史

内容加载中请稍等...

使用广义奇-超位Ⅱ的一阶定理证明

参考文献7

相关作者

相关机构

相关主题

浏览历史