KUCHYŇKA, Petr a Jiří RACLAVSKÝ. Completeness in partial type theory. Journal of Logic and Computation. Oxford, UK: Oxford University Press, 2024, roč. 34, č. 1, s. 1-32. ISSN 0955-792X. Dostupné z: https://dx.doi.org/10.1093/logcom/exac089. |
Další formáty:
BibTeX
LaTeX
RIS
@article{2363117, author = {Kuchyňka, Petr and Raclavský, Jiří}, article_location = {Oxford, UK}, article_number = {1}, doi = {http://dx.doi.org/10.1093/logcom/exac089}, keywords = {partial type theory; completeness proof; partiality; natural deduction; higher-order logic; hyperintensionality}, language = {eng}, issn = {0955-792X}, journal = {Journal of Logic and Computation}, note = {WOS:000936329300001}, title = {Completeness in partial type theory}, url = {https://doi.org/10.1093/logcom/exac089}, volume = {34}, year = {2024} }
TY - JOUR ID - 2363117 AU - Kuchyňka, Petr - Raclavský, Jiří PY - 2024 TI - Completeness in partial type theory JF - Journal of Logic and Computation VL - 34 IS - 1 SP - 1-32 EP - 1-32 PB - Oxford University Press SN - 0955792X N1 - WOS:000936329300001 KW - partial type theory KW - completeness proof KW - partiality KW - natural deduction KW - higher-order logic KW - hyperintensionality UR - https://doi.org/10.1093/logcom/exac089 N2 - The present paper provides a completeness proof for a system of higher-order logic framed within partial type theory. The framework is a modification of Tichý’s extension of Church’s simple type theory, equipped with his innovative natural deduction system in sequent style. The system deals with both total and partial (multiargument) functions-as-mappings and also accommodates algorithmic computations arriving at various objects of the framework. The partiality of a function or a failure of a computation is not represented by a postulated null object such as the third truth value. The logical operators of the system are classical. Another welcome feature of this expressive system is that its consequence relation is monotonic. ER -
KUCHYŇKA, Petr a Jiří RACLAVSKÝ. Completeness in partial type theory. \textit{Journal of Logic and Computation}. Oxford, UK: Oxford University Press, 2024, roč.~34, č.~1, s.~1-32. ISSN~0955-792X. Dostupné z: https://dx.doi.org/10.1093/logcom/exac089.
|