模态逻辑D演绎过程的化简规则

The Reducing Rules of Deducing ProceduRe in Modal Logic D

以分析模态逻辑中文字公式的极性为基础，将经典逻辑的Ｄａｖｉｓ－ｐｕｔｎａｍ纯文字化简规则推广到了命题模态逻辑Ｄ系统的自动演绎中，并给出了一些刻划Ｄ逻辑自动演绎特征的化简规则，这些化简规则通过对公式、子公式和公式集的有效性（或不可满足性）的有条件的判断，进行证明过程的剪枝和化简，以提高Ｄ逻辑自动演绎的效率；这些化简规则都是依据公式（集）本身的结构特征，可用于Ｄ逻辑的任意一种推理实现系统，在机器上是容易实现的。

This paper generalizes the classical Davis-putnam pure literal rules to propositional modallogic D and presents some reducing rules that describe the characters of the deducing procedure inmodal logic D. These reducing rules simplify the proof search tree by checking up the validity(or un-satisfiability)of the formulae under certain conditions so as to improve the efficiency of the deductionin modal logic D. Based on the structure characters of the formulae,these reducing rules can be usedin any automatic reasoning system of modal logic D,and can be implemented easily.