Substituční Fregovské a rozšířené Fregovské důkazové systémy v neklasických logikách
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F09%3A00323651" target="_blank" >RIV/67985840:_____/09:00323651 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Substitution Frege and extended Frege proof systems in non-classical logics
Popis výsledku v původním jazyce
We investigate the substitution Frege (SF) proof system and its relationship to extended Frege (EF) in the context of modal and superintuitionistic (si) propositional logics. We show that EF is p-equivalent to tree-like SF, and we develop a "normal form"for SF-proofs. We establish connections between SF for a logic L, and EF for certain bimodal expansions of L. We then turn attention to specific families of modal and si logics. We prove p-equivalence of EF and SF for all extensions of KB, all tabular logics, all logics of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual EF system for classical logic with respect to a naturally defined translation. On the other hand, we establish exponential speed-up of SF over EF for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš.
Název v anglickém jazyce
Substitution Frege and extended Frege proof systems in non-classical logics
Popis výsledku anglicky
We investigate the substitution Frege (SF) proof system and its relationship to extended Frege (EF) in the context of modal and superintuitionistic (si) propositional logics. We show that EF is p-equivalent to tree-like SF, and we develop a "normal form"for SF-proofs. We establish connections between SF for a logic L, and EF for certain bimodal expansions of L. We then turn attention to specific families of modal and si logics. We prove p-equivalence of EF and SF for all extensions of KB, all tabular logics, all logics of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual EF system for classical logic with respect to a naturally defined translation. On the other hand, we establish exponential speed-up of SF over EF for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš.
Klasifikace
Druh
J<sub>x</sub> - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP obor
BA - Obecná matematika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/IAA1019401" target="_blank" >IAA1019401: Teorie, důkazy a výpočetní složitost</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2009
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
Annals of Pure and Applied Logic
ISSN
0168-0072
e-ISSN
—
Svazek periodika
159
Číslo periodika v rámci svazku
2
Stát vydavatele periodika
NL - Nizozemsko
Počet stran výsledku
48
Strana od-do
—
Kód UT WoS článku
000266337700001
EID výsledku v databázi Scopus
—