| 基于类型理论的面向对象多步证明系统 |
| |
| 引用本文： | 蔡家楣. 基于类型理论的面向对象多步证明系统[J]. 计算机工程, 1998, 24(12): 27-29,34 |
| |
| 作者姓名： | 蔡家楣 |
| |
| 作者单位： | 浙江工业大学信息工程学院,杭州,310014 |
| |
| 基金项目： | 国家高技术研究发展计划(863计划)，浙江省自然科学基金，，，， |
| |
| 摘 要： | 介绍基于扩展构造型演算的交互式多步证明系统。该系统中以函数式语言ＭＬ为开发环境，建立了ＥＣＣ的项、规则证明策略和证明管理机制的描述，并引入规约类型、类类型、类和对象的表示，为面向对象的程序规约和定理证明系统的结合进行了一些探索。
|
| 关 键 词： | 面向对象 程序设计 定理证明 类型理论 |
A Object-oriented Multiverse Proover Based on Type Theory |
| |
| Cai Jiamei. A Object-oriented Multiverse Proover Based on Type Theory[J]. Computer Engineering, 1998, 24(12): 27-29,34 |
| |
| Authors: | Cai Jiamei |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
