%0 Journal Article
%T 证明策略及其有效性问题
%A 何锫？
%J 软件学报
%P 23-30
%D 1991
%X incaps(interactivcomputer-aidedprovingsystem)是一个面向时序逻辑的交互式计算机辅助证明系统。本文简要介绍了其证明策略(tactics,tacticals)的类别、结构,并在引入证明策略的层次数、函数树及树上b函数等新概念前提下,深入探讨和证明了in-caps证明策略的有效性问题。
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=19910404&flag=1