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

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