引用本文:李卫华,张黔,张亮,刘娟.归纳法模式的自动生成.软件学报,1996,7(3):168-174
【打印本页】   【下载PDF全文】   查看/发表评论  【EndNote】   【RefMan】   【BibTex】
←前一篇|后一篇→ 过刊浏览    高级检索
本文已被:浏览 4453次   下载 5592 本文二维码信息
码上扫一扫!
分享到: 微信 更多
归纳法模式的自动生成
李卫华1, 张黔1, 张亮1, 刘娟1
武汉大学计算机科学系,武汉,430072
摘要:
本文介绍归纳法推理系统的核心──归纳法模式的自动生成程序.该程序从递归函数定义出发,自动生成归纳法模板;从待证定理出发,借助归纳法模板,自动生成归纳法模式和归纳法公式.该系统已在微机上用编译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.