On the proof complexity of logics of bounded branching
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F23%3A00560276" target="_blank" >RIV/67985840:_____/23:00560276 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1016/j.apal.2022.103181" target="_blank" >https://doi.org/10.1016/j.apal.2022.103181</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.apal.2022.103181" target="_blank" >10.1016/j.apal.2022.103181</a>
Alternative languages
Result language
angličtina
Original language name
On the proof complexity of logics of bounded branching
Original language description
We investigate the proof complexity of extended Frege (EF) systems for basic transitive modal logics (K4, S4, GL, ...) augmented with the bounded branching axioms BB_k. First, we study feasibility of the disjunction property and more general extension rules in EF systems for these logics: we show that the corresponding decision problems reduce to total coNP search problems (or equivalently, disjoint NP pairs, in the binary case), more precisely, the decision problem for extension rules is equivalent to a certain special case of interpolation for the classical EF system. Next, we use this characterization to prove superpolynomial (or even exponential, with stronger hypotheses) separations between EF and substitution Frege (SF) systems for all transitive logics contained in S4.2GrzBB_2 or GL.2BB_2 under some assumptions weaker than PSPACE ne NP. We also prove analogous results for superintuitionistic logics: we characterize the decision complexity of multi-conclusion Visser's [...]
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10101 - Pure mathematics
Result continuities
Project
<a href="/en/project/GA19-05497S" target="_blank" >GA19-05497S: Complexity of mathematical proofs and structures</a><br>
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2023
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Annals of Pure and Applied Logic
ISSN
0168-0072
e-ISSN
1873-2461
Volume of the periodical
174
Issue of the periodical within the volume
1
Country of publishing house
NL - THE KINGDOM OF THE NETHERLANDS
Number of pages
54
Pages from-to
103181
UT code for WoS article
000844079500001
EID of the result in the Scopus database
2-s2.0-85135951741