%0 Journal Article
%T 标记模态归结推理*
%A 孙吉贵？
%A 刘叙华？
%J 软件学报
%P 156-162
%D 1996
%X 为了克服l.farinasdelcerro等人的命题模态归结方法过多的符号冗余，我们增加了一条两个可能算子约束下公式的归结规则，称之为标记模态归结方法．证明了标记模态归结的可靠性与完备性．这种新模态归结方法具有下述特点;归结式未必是其父子句的逻辑结果，但却是输入于句集的逻辑结果．因而是可靠的．同时，我们在机器上实现了实验系统．实验结果表明标记模态归结比p.enjalbert等人的模态归结几乎快10倍．
%K 命题模态逻辑
%K 模态归结
%K 标记模态归结
%K 自动推理．
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=1996s122&flag=1