Strong Normalization for Truth Table Natural Deduction
| Autor: | Geuvers, H., Giessen, I. van der, Hurkens, Tonny, Altenkirch, T., Schubert, A. |
|---|---|
| Přispěvatelé: | LS Formeel redeneren, OFR - Theoretical Philosophy |
| Rok vydání: | 2019 |
| Předmět: |
Normalization (statistics)
Algebra and Number Theory Natural deduction business.industry permutation conversion Truth table strong normalization intuitionistic logic computer.software_genre Theoretical Computer Science TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Software Science truth tables Artificial intelligence natural deduction business computer detour conversion Natural language processing Information Systems Mathematics |
| Zdroj: | Fundamenta Informaticae, 170, 139-176 Fundamenta Informaticae, 170(1-3), 139 Fundamenta Informaticae, 170, 1-3, pp. 139-176 |
| ISSN: | 1875-8681 0169-2968 |
| DOI: | 10.3233/fi-2019-1858 |
| Popis: | 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 conversionpreserving 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|