具有子公式性质的命题达米特逻辑的终止演算
Terminating Calculi for Propositional Dummett Logic with Subformula Property
摘要：
本文给出了两个满足子公式性质的命题Dummett逻辑的终止表演算。我们演算的思想依赖于Dummett逻辑的线性有序Kripke语义。第一个演算在两个语义层面上工作：现在和下一个可能世界。第二个演算采用通常的对象语言的Tableau系统，并利用一个属性的建设的完整性定理，引入一个检查，这是一种替代循环检查机制。
英文摘要：
In this paper we present two terminating tableau calculi for propositional Dummett logic obeying the subformula property. The ideas of our calculi rely on the linearly ordered Kripke semantics of Dummett logic. The first calculus works on two semantical levels: the present and the next possible world. The second calculus employs the usual object language of tableau systems and exploits a property of the construction of the completeness theorem to introduce a check which is an alternative to loop check mechanisms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
