| 摘要: |
| 本文介绍归纳法推理系统的核心──归纳法模式的自动生成程序.该程序从递归函数定义出发,自动生成归纳法模板;从待证定理出发,借助归纳法模板,自动生成归纳法模式和归纳法公式.该系统已在微机上用编译LISP语言实现. |
| 关键词: 归纳法模板 归纳法模式 归纳法推理 |
| DOI: |
| 分类号: |
| 基金项目:本研究得到国家863高科技项目和国家教委跨世纪优秀人才基金资助. |
|
| AUTOMATIC GENERATION OF INDUCTION SCHEMA |
|
Li Weihua,Zhang Qian,Zhang Liang,Liu Juan
|
| Abstract: |
| This paper discusses the kernel program of an induction inference system the automatic generator of induction schema. Starting from the definition of a recursive function, the system generates the induction template automatically. Starting from the theorem to be proved, it can also automatically produce candidate induction schema and formula by using the template. The system has been implemented on microcomputers. |
| Key words: Induction template induction schema induction inference. |