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