模态归结弱包含删除策略

本文提出了一种模态归结的弱包含删除策略，证明了使用弱包含删除策略模态归结的完备性．从而，将Ａｕｆｆｒａｙ等人提出的开问题（ＯｐｅｎＰｒｏｂｌｅｍ）——模态归结包含删除策略的完备性向前推进了一步．

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

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

标记模态归结的推广

本文将作者提出的高效的命题模态Ｄ逻辑的标记模态归结方法推广到了命题模态逻辑Ｋ，Ｋ４，Ｄ４，Ｔ，Ｓ４系统，建立了上述命题模态逻辑的标记归结形式系统ＭＲＫ，ＭＲＫ４，ＭＲＤ４，ＭＲＴ，ＭＲＳ４．并用转换子句模式的方法，借助于标记模态归结对命题模态Ｄ逻辑的可靠性结果，证明了标记模态归结系统ＭＲＫ，ＭＲＫ４，ＭＲＤ４，ＭＲＴ，ＭＲＳ４分别关于命题模态逻辑Ｋ，Ｋ４，Ｄ４，Ｔ，Ｓ４的可靠性．进而得到了它们的完备性．

标记模态归结推理

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

关于Cialdea一阶模态归结系统

指出了Ｃｉａｌｄｅａ一阶模态逻辑归结系统是不完备的．为了确保推理系统的完备性，给出了Ｃｉａｌｄｅａ系统的两种修正方法．

强模态归结

研究了命题模态逻辑Ｋ，Ｋ４，Ｄ，Ｄ４，Ｔ，Ｓ４的“”型模态逻辑结果的自动推理．提出了证明“”型模态逻辑结果的归结推理方法─—强模态归结．证明了强模态归结的可靠性与完备性．

命题模态归结的一种变型

本文给出了模态子句集的标准子句集概念，提出了一种基于标准子句集的模态归结方法的变型，称之为标准模态归结．证明了任意模态子句集恒假当且仅当存在从它的标准子句集出发，使用标准模态归结推出空子句的演绎．从而证明了对于不可满足标准予句集、标准模态归结是完备的．这种标准模态归结，推理规则简单、直观且容易实现．

一种新的模态归结

本文首先给出了一种标准子句的定义，在其基础上定义了命题模态逻辑系统Ｓ５的子句集的可归结形式．证明了任意模态Ｓ５子句集不可满足的充要条件为在其可归结形式上可归结出空子句．