结构化证明搜索

本文在简介证明开发环境的元语言ＴＭＬ之后，提出两类结构化设施；模块化机制为元级程序设计提供模块化手段；抽象理论机制用来描述定理证明赖以进行的背景理论．联合使用模块机制和结构化理论描述，系统可自动实现结构化证明搜索