%0 Journal Article
%T 区间逻辑的一个辅助证明工具
%A 王戟
%A 胡成军
%A 陈火旺
%J -
%D 2000
%X DC/P(duration calculus prover)是一族实时区间逻辑的辅助定理证明工具.它采用Gentzen风格相继式演算作为基本证明系统,并结合项重写、自动判定算法等技术以提高证明的自动化程序.该文介绍了DC/P的语义编码方法、采用的相继式证明系统及实现技术,并给出了应用实例
%K 邻域逻辑
%K 区间时序逻辑
%K 均值演算
%K 时段演算
%K 相继式演算
%K 定理证明.
%U http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?file_no=20000116&flag=1