%0 Journal Article
%T 结构化证明搜索
%A 谭庆平
%A 陈火旺
%J -
%D 1995
%X 本文在简介证明开发环境的元语言ＴＭＬ之后，提出两类结构化设施；模块化机制为元级程序设计提供模块化手段；抽象理论机制用来描述定理证明赖以进行的背景理论．联合使用模块机制和结构化理论描述，系统可自动实现结构化证明搜索
%K 结构化理论
%K 证明开发
%K 类型理论
%K 元程序设计
%U http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?file_no=19950105&flag=1