Loop-free calculus for modal logic S4. I

被引：0

作者：

Julius Andrikonis

机构：

[1] Vilnius University,Faculty of Mathematics and Informatics

来源：

Lithuanian Mathematical Journal | 2012年 / 52卷

关键词：

modal logic; loop-free calculus; sequent calculus; 03B45;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

In the article, loop-free calculus for modal logic S4 is presented. To restrict applications of reflexivity and transitivity rules, several types of indexes are used. The use of indexes replaces the need to keep the history of previous applications of the rules. The article details the purpose of each type of index and proves that derivation search in the calculus is finite.

引用

页码：1 / 12

页数：11

共 8 条

[1]

Ladner RE(1977)The computational complexity of provability in systems of modal propositional logic SIAM J. Comput. 6 467-480

[2]

Leszczyńska-Jasion D(2009)A loop-free decision procedure for modal propositional logics K4, S4, and S5 J. Philos. Log. 38 151-177

[3]

Ohnishi M(1957)Gentzen method in modal calculi Osaka J. Math. 9 113-130

[4]

Matsumoto K(2010)A new method to obtain termination in backward proof search for modal logic S4 J. Log. Comput. 20 353-379

[5]

Pliuškevičius R(2010)Corrigendum: A new method to obtain termination in backward proof search for modal logic S4 J. Log. Comput. 20 381-387

[6]

Pliuškevičienė A(undefined)undefined undefined undefined undefined-undefined

[7]

Pliuškevičius R(undefined)undefined undefined undefined undefined-undefined

[8]

Pliuškevičienė A(undefined)undefined undefined undefined undefined-undefined

← 1 →