论文标题
关于有限分支的逻辑的证据复杂性
On the proof complexity of logics of bounded branching
论文作者
论文摘要
我们研究了使用有限的分支公理$ \ Mathbf {bb} _K $增强的基本传播模态逻辑（K4，S4，GL，...）的扩展Frege（EF）系统的证明复杂性。首先，我们研究了这些逻辑的EF系统中分离属性和更一般的扩展规则的可行性：我们表明，相应的决策问题减少到总概括搜索问题（或等效地，在二进制案例中，脱节NP NP对）；更确切地说，扩展规则的决策问题等同于经典EF系统的某些特殊情况。接下来，我们使用这种表征来证明EF和替换频率（SF）在$ \ Mathbf {s4.2grzbb_2} $或$ \ MathBf {gl.2bb_2} $下的所有传递逻辑中的EF和替代频率（SF）之间的分离（SF）弱点{s4.2grzbb_2} $ neys prof $ free（SF）free（SF）frege（SF）free（SF）{gl.2bb_2} $ privants p pl.2bb_2} $， NP} $。我们还证明了超持续学逻辑的类似结果：我们表征了gabbay-de jongh逻辑$ \ mathbf t_k $在EF系统中多结论Visser规则的决策复杂性，并且我们在$ \ mathbff {t_2 _cc {t_2 _cc}中均包含EF和SF之间的有条件分离。
We investigate the proof complexity of extended Frege (EF) systems for basic transitive modal logics (K4, S4, GL, ...) augmented with the bounded branching axioms $\mathbf{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 $\mathbf{S4.2GrzBB_2}$ or $\mathbf{GL.2BB_2}$ under some assumptions weaker than $\mathrm{PSPACE \ne NP}$. We also prove analogous results for superintuitionistic logics: we characterize the decision complexity of multi-conclusion Visser's rules in EF systems for Gabbay--de Jongh logics $\mathbf T_k$, and we show conditional separations between EF and SF for all intermediate logics contained in $\mathbf{T_2 + KC}$.
