# From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction

Bulletin of the Section of Logic (2017)

- Volume: 46, Issue: 1/2
- ISSN: 0138-0680

## Access Full Article

top## Abstract

top## How to cite

topJan von Plato. "From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction." Bulletin of the Section of Logic 46.1/2 (2017): null. <http://eudml.org/doc/295558>.

@article{JanvonPlato2017,

abstract = {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.},

author = {Jan von Plato},

journal = {Bulletin of the Section of Logic},

keywords = {proof systems; linear natural deduction; Gentzen; Jaśkowski},

language = {eng},

number = {1/2},

pages = {null},

title = {From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction},

url = {http://eudml.org/doc/295558},

volume = {46},

year = {2017},

}

TY - JOUR

AU - Jan von Plato

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

SP - null

AB - 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.

LA - eng

KW - proof systems; linear natural deduction; Gentzen; Jaśkowski

UR - http://eudml.org/doc/295558

ER -

## References

top- [1] H. Curry, (1965) Remarks on inferential deduction, [in:] A. Tyminiecka (ed.), Contributions to Logic and Methodology in Honor of J. M. Bochenski, North-Holland (1965), pp. 45–72.
- [2] G. Gentzen, Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 39 (1934-35), pp. 176–210 and 405-431.
- [3] S. Jaśkowski, On the rules of supposition in formal logic (1934), as reprinted [in:] S. McCall (ed.), Polish Logic 1920–1939, pp. 232–258, Oxford U. P. 1967.
- [4] J. von Plato, Natural deduction with general elimination rules, Archive for Mathematical Logic, vol. 40 (2001), pp. 541–567.
- [5] J. von Plato, Elements of Logical Reasoning, Cambridge, 2013.
- [6] D. Prawitz, ABC i Symbolisk Logik, Mimeographed compendium. Later expanded and printed editions with Bokförlaget Thales, 1973.

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.