Cialdea一阶模态归结系统的不完备性及其改进

摘要

Cialdea的一阶模态D逻辑归结系统具有符号冗余较少和机器上较容易实现等优点,但它是不完备的.本文中,我们改进了Cialdea归结系统,引入了两个可能算子约束的公式间的归结规则,得到了一种新的一阶模态D逻辑的归结系统,记为FMRD.FMRD很好地保持了Cialdea归结系统的优点,同时,我们证明了FMRD的可靠性与完备性.