标记模态归结推理

为了克服Ｌ．Ｆａｒｉｎａｓ ｄｅｌ Ｃｅｒｒｏ等人的命题模态归方法过多的符号冗余，我们增加了一条两个可能处子约束下公式的归结规则，称之为樗模态旭结方法，证明了标记模态归结的可靠性与完备性，这种新模态归结方法具有下述特点：归结式未必是父子句的逻辑结果，但却是输入子句集的逻辑结果，因而是可靠的，同时我们在机器上实现了实验系统。实验结果表明标记模态归结比Ｐ．Ｅｎｊａｌｂｅｒｔ等人的模态归结几乎快１０倍。