From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction
Bulletin of the Section of Logic, Tome 46 (2017) no. 1-2 Cet article a éte moissonné depuis la source Library of Science

Voir la notice de l'article

The way from linearly written derivations in natural deduction, introduced by Jaskowski and often used in textbooks, is a straightforward root-first translation. The other direction, instead, is tricky, because of the partially ordered assumption formulas in a tree that can get closed by the end of a derivation. An algorithm is defined that operates alternatively from the leaves and root of a derivation and solves the problem.
Keywords: proof systems, linear natural deduction, Gentzen, Jaśkowski
@article{BSL_2017_46_1-2_a2,
     author = {von Plato, Jan},
     title = {From {Gentzen} to {Jaskowski} and {Back:} {Algorithmic} {Translation} of {Derivations} {Between} the {Two} {Main} {Systems} of {Natural} {Deduction}},
     journal = {Bulletin of the Section of Logic},
     year = {2017},
     volume = {46},
     number = {1-2},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a2/}
}
TY  - JOUR
AU  - von Plato, Jan
TI  - From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction
JO  - Bulletin of the Section of Logic
PY  - 2017
VL  - 46
IS  - 1-2
UR  - http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a2/
LA  - en
ID  - BSL_2017_46_1-2_a2
ER  - 
%0 Journal Article
%A von Plato, Jan
%T From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction
%J Bulletin of the Section of Logic
%D 2017
%V 46
%N 1-2
%U http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a2/
%G en
%F BSL_2017_46_1-2_a2
von Plato, Jan. From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction. Bulletin of the Section of Logic, Tome 46 (2017) no. 1-2. http://geodesic.mathdoc.fr/item/BSL_2017_46_1-2_a2/