Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Fundamenta Informaticae

1 2019

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: truth tables

Sortuj według:

Ogranicz wyniki do:

Strong Normalization for Truth Table Natural Deduction

Geuvers Herman, van der Giessen Iris, Hurkens Tonny

Fundamenta Informaticae

2019

Vol. 170, nr 1-3

139--176

We present a proof of strong normalization of proof-reduction in a general system of natural deduction called truth table natural deduction. In previous work, we have defined truth table natural deduction, which is a method for deriving intuitionistic derivation rules for a connective from its truth table. This yields natural deduction rules for each connective separately. Moreover, these rules adhere to a standard format which gives rise to a general notions of detour and permutation conversion for natural deductions. The aim is to remove all convertibilities and obtain a deduction in normal form. In general, conversion of truth table natural deductions is non-deterministic, which makes it more challenging to study. It has already been shown that this conversion is weakly normalizing. To prove strong normalization, we construct a conversion-preserving translation from deductions to terms in an extension of simply typed lambda calculus which we call parallel simply typed lambda calculus and which we prove to be strongly normalizing. This makes it possible to get a grip on the non-deterministic character of conversion in the intuitionistic truth table natural deduction system.