Completeness in partial type theory
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14210%2F24%3A00139346" target="_blank" >RIV/00216224:14210/24:00139346 - isvavai.cz</a>
Výsledek na webu
<a href="https://doi.org/10.1093/logcom/exac089" target="_blank" >https://doi.org/10.1093/logcom/exac089</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1093/logcom/exac089" target="_blank" >10.1093/logcom/exac089</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Completeness in partial type theory
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Completeness in partial type theory
Popis výsledku anglicky
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.
Klasifikace
Druh
J<sub>imp</sub> - Článek v periodiku v databázi Web of Science
CEP obor
—
OECD FORD obor
60301 - Philosophy, History and Philosophy of science and technology
Návaznosti výsledku
Projekt
<a href="/cs/project/GA19-12420S" target="_blank" >GA19-12420S: Hyperintenzionální význam, teorie typů a logická dedukce</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2024
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název periodika
Journal of Logic and Computation
ISSN
0955-792X
e-ISSN
1465-363X
Svazek periodika
34
Číslo periodika v rámci svazku
1
Stát vydavatele periodika
GB - Spojené království Velké Británie a Severního Irska
Počet stran výsledku
32
Strana od-do
1-32
Kód UT WoS článku
000936329300001
EID výsledku v databázi Scopus
2-s2.0-85182900627