论文部分内容阅读
Ｃｉａｌｄｅａ的－阶模态Ｄ逻辑归结系统具有符号冗余较少和机器上较容易实现等优点，但它是不完备的。本文中，我们改进了Ｃｉａｌｄｅａ归结系统，引入了两个可能算子约束的公式间的归结规则，得到了一种新的一阶模态Ｄ逻辑的归结系统，记为ＦＭＲＤ．ＦＭＲＤ很好地保持了Ｃｉａｌｄｅａ归结系统的优点，同时，我们证明了ＦＭＲＤ的可靠性与完备性。