| 摘要: |
| 本文在简介证明开发环境的元语言ＴＭＬ之后，提出两类结构化设施；模块化机制为元级程序设计提供模块化手段；抽象理论机制用来描述定理证明赖以进行的背景理论．联合使用模块机制和结构化理论描述，系统可自动实现结构化证明搜索． |
| 关键词: 结构化理论，证明开发，类型理论，元程序设计 |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到“863”高技术计划及国家自然科学基金的部分资助. |
|
| STRUCTURED PROOF SEARCH |
|
Tan Qingping,Chen Huowang
|
| Abstract: |
| This paper describes TML, a metalanguage intended for proof development and program design environments. The abstract theory and meta-module mechanisms are presented in TML to allow a good modularization of proof development and make it possible to direct the search for a proof in well-structured theories mechanically. |
| Key words: Structured theory, proof development, type theory, metaprogramming. |
