基于类型理论的面向对象多步证明系统

摘要：

介绍基于扩展构造型演算的交互式多步证明系统.该系统中以函数式语言ML为开发环境,建立了ECC的项、规则证明策略和证明管理机制的描述,并引入规约类型,类类型、类和对象的表示,为面向对象的程序规约和定理证明系统的结合进行了一些探索.

关键词：扩展构造演算、面向对象程序设计、定理证明

所属期刊栏目：24

分类号：TP3(计算技术、计算机技术)

资助基金：国家高技术研究发展计划863计划;浙江省自然科学基金

在线出版日期：2005-08-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：27-29,34