On the proof complexity of logics of bounded branching

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

On the proof complexity of logics of bounded branching

Popis výsledku v původním jazyce

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 [...]

Název v anglickém jazyce

On the proof complexity of logics of bounded branching

Popis výsledku anglicky

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 [...]

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

<a href="/cs/project/GA19-05497S" target="_blank" >GA19-05497S: Složitost matematických důkazů a struktur</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2023

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ů

Název periodika

Annals of Pure and Applied Logic

ISSN

0168-0072

e-ISSN

1873-2461

Svazek periodika

174

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

54

Strana od-do

103181

Kód UT WoS článku

000844079500001

EID výsledku v databázi Scopus

2-s2.0-85135951741