Další formáty:
BibTeX
LaTeX
RIS
@proceedings{1793024,
author = {Raclavský, Jiří and Kuchyňka, Petr},
booktitle = {Logic and Applications XX (LAP2021), Dubrovnik, September 20-24, 2021},
keywords = {partial type theory; natural deduction; evaluation terms},
language = {eng},
note = {(conf.)},
title = {Natural Deduction for Partial Type Theory with 'Evaluation Terms'},
url = {http://imft.ftn.uns.ac.rs/math/cms/LAP2021},
year = {2021}
}
TY - CONF
ID - 1793024
AU - Raclavský, Jiří - Kuchyňka, Petr
PY - 2021
TI - Natural Deduction for Partial Type Theory with 'Evaluation Terms'
N1 - (conf.)
KW - partial type theory
KW - natural deduction
KW - evaluation terms
UR - http://imft.ftn.uns.ac.rs/math/cms/LAP2021
N2 - 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*.
ER -
RACLAVSKÝ, Jiří a Petr KUCHYŇKA. Natural Deduction for Partial Type Theory with 'Evaluation Terms'. In \textit{Logic and Applications XX (LAP2021), Dubrovnik, September 20-24, 2021}. 2021.
|
