Počet záznamů: 1
Substitution Frege and extended Frege proof systems in non-classical logics
- 1.
SYSNO ASEP 0323651 Druh ASEP J - Článek v odborném periodiku Zařazení RIV J - Článek v odborném periodiku Poddruh J Článek ve WOS Název Substitution Frege and extended Frege proof systems in non-classical logics Překlad názvu Substituční Fregovské a rozšířené Fregovské důkazové systémy v neklasických logikách Tvůrce(i) Jeřábek, Emil (MU-W) RID, SAI, ORCID Zdroj.dok. Annals of Pure and Applied Logic. - : Elsevier - ISSN 0168-0072
Roč. 159, č. 2 (2009), s. 1-48Poč.str. 48 s. Jazyk dok. eng - angličtina Země vyd. NL - Nizozemsko Klíč. slova propositional proof complexity ; Frege system ; model logic Vědní obor RIV BA - Obecná matematika CEP IAA1019401 GA AV ČR - Akademie věd CEZ AV0Z10190503 - MU-W (2005-2011) UT WOS 000266337700001 Anotace 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š. Pracoviště Matematický ústav Kontakt Jarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757 Rok sběru 2009
Počet záznamů: 1