%0 Journal Article
%T STRUCTURED PROOF SEARCH<br>结构化证明搜索
%A Tan Qingping
%A Chen Huowang
%A <br>谭庆平
%A 陈火旺
%J 软件学报
%D 1995
%I 
%X 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.
%K Structured theory
%K proof development
%K type theory
%K metaprogramming<br>结构化理论，证明开发，类型理论，元程序设计
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=F8A2EDD756A0AA9D064B25CC54C65540&yid=BBCD5003575B2B5F&vid=B31275AF3241DB2D&iid=CA4FD0336C81A37A&sid=27746BCEEE58E9DC&eid=1371F55DA51B6E64&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=14