| Attributes | Values |
|---|
| rdf:type
| |
| Description
| - 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 %22normal form%22 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š.
- 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 %22normal form%22 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š. (en)
- Zkoumáme substituční Fregovský (SF) důkazový systém a jeho vztah k rozšířenému Fregovskému (EF) systému v kontextu modálních a superintuicionistických (si) výrokových logik. Ukážeme, že EF je p-ekvivalentní stromovému SF a vyvineme %22normální formu%22 pro SF-důkazy. Prokážeme souvislosti mezi SF pro logiku L0 a EF pro jistá bimodální rozšíření L. Dále se zaměříme na konkrétní třídy modálních a si logik. Dokážeme p-ekvivalenci EF a SF pro všechna rozšíření KB, všechny tabulární logiky, všechny logiky, všechny logiky konečné hloubky a šířky a typické příklady logik konečné šířky a nekonečné hloubky. Ve většině případů vlastně ukážeme ekvivalenci s obvyklým EF systémem pro klasickou logiku vzhledem k přirozeně definovanému překladu. Na druhou stranu dokážeme exponenciální zrychlení SF and EF pro všechny modální a si logiky s nekonečným větvením, rozšířením nedávných dolních odhadů P. Hrubeše. (cs)
|
| Title
| - Substitution Frege and extended Frege proof systems in non-classical logics
- Substitution Frege and extended Frege proof systems in non-classical logics (en)
- Substituční Fregovské a rozšířené Fregovské důkazové systémy v neklasických logikách (cs)
|
| skos:prefLabel
| - Substitution Frege and extended Frege proof systems in non-classical logics
- Substitution Frege and extended Frege proof systems in non-classical logics (en)
- Substituční Fregovské a rozšířené Fregovské důkazové systémy v neklasických logikách (cs)
|
| skos:notation
| - RIV/67985840:_____/09:00323651!RIV09-AV0-67985840
|
| http://linked.open...avai/riv/aktivita
| |
| http://linked.open...avai/riv/aktivity
| - P(IAA1019401), Z(AV0Z10190503)
|
| http://linked.open...iv/cisloPeriodika
| |
| http://linked.open...vai/riv/dodaniDat
| |
| http://linked.open...aciTvurceVysledku
| |
| http://linked.open.../riv/druhVysledku
| |
| http://linked.open...iv/duvernostUdaju
| |
| http://linked.open...titaPredkladatele
| |
| http://linked.open...dnocenehoVysledku
| |
| http://linked.open...ai/riv/idVysledku
| - RIV/67985840:_____/09:00323651
|
| http://linked.open...riv/jazykVysledku
| |
| http://linked.open.../riv/klicovaSlova
| - propositional proof complexity; Frege system; model logic (en)
|
| http://linked.open.../riv/klicoveSlovo
| |
| http://linked.open...odStatuVydavatele
| |
| http://linked.open...ontrolniKodProRIV
| |
| http://linked.open...i/riv/nazevZdroje
| - Annals of Pure and Applied Logic
|
| http://linked.open...in/vavai/riv/obor
| |
| http://linked.open...ichTvurcuVysledku
| |
| http://linked.open...cetTvurcuVysledku
| |
| http://linked.open...vavai/riv/projekt
| |
| http://linked.open...UplatneniVysledku
| |
| http://linked.open...v/svazekPeriodika
| |
| http://linked.open...iv/tvurceVysledku
| |
| http://linked.open...ain/vavai/riv/wos
| |
| http://linked.open...n/vavai/riv/zamer
| |
| issn
| |
| number of pages
| |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)