摘要
１引言归纳法是刻划软硬件行为和性质的一种重要方法，归纳证明的自动化始终是一个研究热点．近二十年来，涌现出了大批证明方法和实验系统．这些成果大致可分为两类：第一类方法使用项结构上的显式归纳论证，其典型工具是１９７９年由Ｂｏｙｅｒ和Ｍｏｏｒｅ提出的ＮＱＴ...
出处
《计算机学报》
EI
CSCD
北大核心
1999年第5期558-560,共3页
Chinese Journal of Computers
基金
国家"九.五"科技攻关计划
国家自然科学基金
上海市高等学校青年科学基金
同被引文献6
-
1Musser D R, Shao Z Q. The tecton concept description language (revised version)[EB/OL], http://www, cs. rpi. edu/-zshao/,2003. 被引量：1
-
2Burstall R. Proving properties of programs by structural induction[J]. Computer Journal, 1969,12 ( 1 ) : 41-48. 被引量：1
-
3Zhang H T,Deepak K, Mukkai S K. A mechanizable induction principle for equation specifications[A]. Proc eading of Ninth International Conference on Automated Deduction[C].Argonne, IL : Springer-Verlag, 1988. 250-265. 被引量：1
-
4Deepak K, Musser D R, Nie X M. An overview of the tectonpro of system[EB/OL], http://www, cs. rpi. edu/～musser/,2003. 被引量：1
-
5Quemada J, Manas J, Vizouez E. Formal Description Techniques[M]. North-Holland : Elsevier Science Publishers, 1991. 被引量：1
-
6钱群力,邵志清,虞慧群.基于关键规则分组优先提取策略的完备化算法及其实现[J].华东理工大学学报（自然科学版）,2000,26(5):451-454. 被引量：1
-
1陈开龙.证明垂直的方法[J].课堂内外（初中版）,2007(12).
-
2冯速.项重写系统等价性的归纳证明[J].计算机科学,2000,27(8):5-7. 被引量：4
-
3钟发荣,孙永强.关于归纳证明的探讨[J].计算机科学,1998,25(5):59-61.
-
4武炳杰.赏析运用斐波那契数列归纳证明的问题[J].中等数学,2008(11):16-18.
-
5袁晓月,黎爽.归纳证明在类型理论中的应用研究[J].江西科学,2015,33(2):248-253.
-
6张欢欢,邵志清,宋国新.基于幂表的并行加法器的归纳验证[J].电子学报,2003,31(6):932-936. 被引量：3
-
7陈庆燕,姚雷博.一个极小不可满足公式子集的构造[J].洛阳理工学院学报（自然科学版）,2011,21(4):77-79.
-
8冯速.项重写系统弱基终止性的归纳证明[J].计算机科学,2001,28(7):105-108. 被引量：4
-
9张静,邵志清.用构造基证明归纳定理[J].华东理工大学学报（自然科学版）,2000,26(5):529-533.
-
10潘国强,虞慧群,宋国新,邵志清.基于控制周期特征式的线性混合自动机验证[J].华东理工大学学报（自然科学版）,2000,26(5):471-476.
