Geodesic
Cut Elimination Theorem for Non-Commutative Hypersequent Calculus
Bulletin of the Section of Logic, Tome 46 (2017) no. 1-2.

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

Hypersequent calculi (HC) can formalize various non-classical logics. In [9] we presented a non-commutative variant of HC for the weakest temporal logic of linear frames Kt4.3 and some its extensions for dense and serial flow of time. The system was proved to be cut-free HC formalization of respective temporal logics by means of Schütte/Hintikka-style semantical argument using models built from saturated hypersequents. In this paper we present a variant of this calculus for Kt4.3 with a constructive syntactical proof of cut elimination.
Keywords: temporal logic, linear time, hypersequent calculus, cut elimination 
@article{BSL_2017_46_1-2_a0,
     author = {Indrzejczak, Andrzej},
     title = {Cut {Elimination} {Theorem} for {Non-Commutative} {Hypersequent} {Calculus}},
     journal = {Bulletin of the Section of Logic},
     publisher = {mathdoc},
     volume = {46},
     number = {1-2},
     year = {2017},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a0/}
}
TY  - JOUR
AU  - Indrzejczak, Andrzej
TI  - Cut Elimination Theorem for Non-Commutative Hypersequent Calculus
JO  - Bulletin of the Section of Logic
PY  - 2017
VL  - 46
IS  - 1-2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a0/
LA  - en
ID  - BSL_2017_46_1-2_a0
ER  - 
%0 Journal Article
%A Indrzejczak, Andrzej
%T Cut Elimination Theorem for Non-Commutative Hypersequent Calculus
%J Bulletin of the Section of Logic
%D 2017
%V 46
%N 1-2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a0/
%G en
%F BSL_2017_46_1-2_a0
Indrzejczak, Andrzej. Cut Elimination Theorem for Non-Commutative Hypersequent Calculus. Bulletin of the Section of Logic, Tome 46 (2017) no. 1-2. http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a0/