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

• Autorzy: Jan von Plato
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

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

• Wydawca: Wydawnictwo Uniwersytetu Łódzkiego
• Czasopismo: Bulletin of the Section of Logic
• Rocznik: 2017
• Tom: 46
• Numer: 1/2

Daty

wydano

2017-06-30

Twórcy

autor

Jan von Plato

Identyfikatory

DOI

10.18778/0138-0680.46.1.2.06