Další formáty:
BibTeX
LaTeX
RIS
@proceedings{1805082, author = {Raclavský, Jiří and Kuchyňka, Petr}, booktitle = {Non-Classical Modal and Predicate Logics (NCMPL2021), Bochum, November 23-26, 2021}, keywords = {completeness; partial type theory; natural deduction}, language = {eng}, note = {(conf.)}, title = {Completeness in Partial Type Theory}, url = {https://sites.google.com/view/ncmpl2021/home}, year = {2021} }
TY - CONF ID - 1805082 AU - Raclavský, Jiří - Kuchyňka, Petr PY - 2021 TI - Completeness in Partial Type Theory N1 - (conf.) KW - completeness KW - partial type theory KW - natural deduction UR - https://sites.google.com/view/ncmpl2021/home N2 - Higher-order logic (HOL), especially simple type theory (STT), are expressive systems of quantification over numerous domains. The expressive power causes incompleteness in standard models, but Henkin proved the completeness of STT w.r.t. to general models. We adjust his procedure and provide a completeness proof for natural deduction system for partial TT called TT*, which is systematically equipped with both total and partial functions, and even with special `evaluation terms' (the system thus treats even a hierarchy of functions-as-computations). ER -
RACLAVSKÝ, Jiří a Petr KUCHYŇKA. Completeness in Partial Type Theory. In \textit{Non-Classical Modal and Predicate Logics (NCMPL2021), Bochum, November 23-26, 2021}. 2021.
|