2021
Natural Deduction for Partial Type Theory with 'Evaluation Terms'
RACLAVSKÝ, Jiří a Petr KUCHYŇKAZákladní údaje
Originální název
Natural Deduction for Partial Type Theory with 'Evaluation Terms'
Autoři
RACLAVSKÝ, Jiří (203 Česká republika, garant, domácí) a Petr KUCHYŇKA (203 Česká republika)
Vydání
Logic and Applications XX (LAP2021), Dubrovnik, September 20-24, 2021, 2021
Další údaje
Jazyk
angličtina
Typ výsledku
Prezentace na konferencích
Obor
60301 Philosophy, History and Philosophy of science and technology
Stát vydavatele
Chorvatsko
Utajení
není předmětem státního či obchodního tajemství
Odkazy
Kód RIV
RIV/00216224:14210/21:00119213
Organizační jednotka
Filozofická fakulta
Klíčová slova anglicky
partial type theory; natural deduction; evaluation terms
Štítky
Příznaky
Mezinárodní význam, Recenzováno
Změněno: 31. 3. 2022 14:13, Ing. Mgr. Zdeňka Jastrzembská, Ph.D.
Anotace
V originále
The talk proposes an expressive natural deduction system in sequent style ND-TT* for a higher-order partial type theory TT*. TT* treats both total and partial functions-as-graphs and also acyclic algorithmic computations, called constructions (of certain objects of TT*). The system is usable e.g. for the analysis of fine-grained hyperintensionality (see e.g. Tichy 1988) and meta-logical notions. The basic part is adjusted from Tichy's 1982 convenient natural deduction system for his partial type theory (for other approaches, see e.g. Farmer 1990, Muskens 1995, Moschovakis 2005). TT* mainly extends his system by admission of 'evaluation terms' (cf. e.g. Tichy 1988, Farmer 2016, Raclavsky 2020). Our ND-TT* provides all basic rules governing those special constructions. Finally, we sketch a Henkin-style completeness proof for ND-TT*.
Návaznosti
| GA19-12420S, projekt VaV |
|