模态逻辑S_5的表推演系统TS_5

Tableaux System TS_5 of the Regular Modal Logic S_5

进一步讨论关于正规模态逻辑S_5的自动定理证明理论与方法.给出了正规模态逻辑S_5的表推演(Tableau)系统TS_(?).证明了该系统的可靠性与完备性。

In this paper we discuss the theory of automated reasoning on the regular modal logic S5 and present the tableau system TS5 of the regular system S5 and show its soundness and completeness.