Geodesic
Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus
Bulletin of the Section of Logic, Tome 45 (2016) no. 2.

Voir la notice de l'article provenant de la source Library of Science

In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi (SC) for S5 the presented system does not introduce any extra devices. Thus it is a standard version of SC but with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form.
Keywords: Modal logic S5, decidability, normal forms, sequent calculus 
@article{BSL_2016_45_2_a4,
     author = {Indrzejczak, Andrzej},
     title = {Simple {Decision} {Procedure} for {S5} in {Standard} {Cut-Free} {Sequent} {Calculus}},
     journal = {Bulletin of the Section of Logic},
     publisher = {mathdoc},
     volume = {45},
     number = {2},
     year = {2016},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2016_45_2_a4/}
}
TY  - JOUR
AU  - Indrzejczak, Andrzej
TI  - Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus
JO  - Bulletin of the Section of Logic
PY  - 2016
VL  - 45
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2016_45_2_a4/
LA  - en
ID  - BSL_2016_45_2_a4
ER  - 
%0 Journal Article
%A Indrzejczak, Andrzej
%T Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus
%J Bulletin of the Section of Logic
%D 2016
%V 45
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2016_45_2_a4/
%G en
%F BSL_2016_45_2_a4
Indrzejczak, Andrzej. Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus. Bulletin of the Section of Logic, Tome 45 (2016) no. 2. http://geodesic.mathdoc.fr/item/BSL_2016_45_2_a4/