| 谭庆平,陈火旺.结构化证明搜索.软件学报,1995,6(1):33-40 |
| 结构化证明搜索 |
| STRUCTURED PROOF SEARCH |
| 投稿时间：1992-06-09 修订日期：1992-11-12 |
| DOI： |
| 中文关键词: 结构化理论，证明开发，类型理论，元程序设计 |
| 英文关键词:Structured theory, proof development, type theory, metaprogramming. |
| 基金项目:本文研究得到“863”高技术计划及国家自然科学基金的部分资助. |
|
| 摘要点击次数: 2858 |
| 全文下载次数: 2735 |
| 中文摘要: |
| 本文在简介证明开发环境的元语言ＴＭＬ之后，提出两类结构化设施；模块化机制为元级程序设计提供模块化手段；抽象理论机制用来描述定理证明赖以进行的背景理论．联合使用模块机制和结构化理论描述，系统可自动实现结构化证明搜索． |
| 英文摘要: |
| 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. |
|
HTML 下载PDF全文 查看/发表评论 下载PDF阅读器 |
