Detailed Information on Publication Record
2021
Natural Deduction for Partial Type Theory with 'Evaluation Terms'
RACLAVSKÝ, Jiří and Petr KUCHYŇKABasic information
Original name
Natural Deduction for Partial Type Theory with 'Evaluation Terms'
Authors
RACLAVSKÝ, Jiří (203 Czech Republic, guarantor, belonging to the institution) and Petr KUCHYŇKA (203 Czech Republic)
Edition
Logic and Applications XX (LAP2021), Dubrovnik, September 20-24, 2021, 2021
Other information
Language
English
Type of outcome
Prezentace na konferencích
Field of Study
60301 Philosophy, History and Philosophy of science and technology
Country of publisher
Croatia
Confidentiality degree
není předmětem státního či obchodního tajemství
References:
RIV identification code
RIV/00216224:14210/21:00119213
Organization unit
Faculty of Arts
Keywords in English
partial type theory; natural deduction; evaluation terms
Tags
Tags
International impact, Reviewed
Změněno: 31/3/2022 14:13, Ing. Mgr. Zdeňka Jastrzembská, Ph.D.
Abstract
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*.
Links
| GA19-12420S, research and development project |
|