ABSTRACT. We study when a sound arithmetic theory $\mathcal S{\supseteq}S^1_2$ with polynomial-time decidable axioms efficiently proves the bounded consistency statements $Con_{\mathcal S{+}\phi}(n)$ for a true sentence $\phi$. Equivalently, we ask when $\mathcal S$, viewed as a proof system, simulates $\mathcal S{+}\phi$. The paper's two unconditional contributions constrain possible characterizations. First, for finitely axiomatized sequential $\mathcal S$, if $EA{\vdash}Con_{\mathcal S}{\rightarrow}Con_{\mathcal S{+}\phi}$, then $\mathcal S$ interprets $\mathcal S{+}\phi$, implying $\mathcal S{\sststile{}{n^{O(1)}}}Con_{\mathcal S}(p(n)){\rightarrow}Con_{\mathcal S{+}\phi}(n)$ for some polynomial $p$, and hence $\mathcal S{\sststile{}{n^{O(1)}}}Con_{\mathcal S{+}\phi}(n)$. Second, if $\mathcal S$ fails to simulate $\mathcal S{+}\phi$ for some true $\phi$, then for all sufficiently large $k$ it also fails for $\phi_{BB}(k)$ asserting the exact value of the $k$-state Busy Beaver function. Informally, any argument showing that $\mathcal S$ fails to simulate some $\mathcal S{+}\phi$ also yields unprovable $\phi_{BB}(k)$ witnessing the same obstruction. These results suggest that relative consistency strength is a serious candidate for governing when simulation is possible, while leaving open whether it is the correct criterion. The paper's central conjectural proposal is that the above sufficient condition is also necessary: if $EA{\not\vdash}Con_{\mathcal S}{\rightarrow}Con_{\mathcal S{+}\phi}$, then for every constant $c{>}0$, $\mathcal S\centernot{\sststile{}{n^c}}Con_{\mathcal S{+}\phi}(n)$. Under this proposal, hardness follows in canonical cases where $\phi$ is $Con_{\mathcal S}$ or a Kolmogorov-randomness axiom. The latter yields further conjectural consequences and extensions.

ABSTRACT. Cook introduced the equational theory PV, whose terms are exactly the polynomial-time functions, to capture the notion of feasibly constructive proofs. Our aim is to develop a 'positive' version of PV which we call posPV, where the terms are the positive polynomial-time functions, that is, the functions computable in polynomial time without using negations. This is a continuation of previous work on uniform monotone complexity, in particular building on a Cobham style characterisation of the positive polynomial functions. We seek to build a framework analogous to that of Cook by providing a polynomial-size translation of posPV proofs into a propositional proof system, and proving that posPV proves the reflection principle for this language.

ABSTRACT. Since their introduction by Atserias, Kolaitis, and Vardi in 2004, proof systems where each line is represented by an ordered binary decision diagram (OBDD) have been intensively studied as they allow to compactly represent Boolean functions. We extend this line of work by considering representation formats that can be even more succinct than OBDDs and have gained a lot of attention in the area of knowledge compilation: sentential decision diagrams (SDDs) and deterministic structured DNNF circuits (d-SDNNFs). We show that both variants can provide strictly smaller refutations of unsatisfiable CNFs than their OBDD counterparts. Furthermore, we investigate the relative strength of these systems depending on which of the three fundamental derivation rules join, reordering, and weakening are allowed. Here we obtain several separations and identify interesting open problems. To streamline our proofs we establish a sat-to-unsat lifting theorem that might be of independent interest: it turns satisfiable CNFs that are hard to represent by SDDs and d-SDNNFs into unsatisfiable CNFs that are hard to refute in the corresponding proof system. This work is accepted for publication at SAT 2026.

ABSTRACT. For line-based propositional proof systems, there is a default way to extend them to proof system for quantified boolean formulas (QBF). For static proof systems, there is no such default method. Most known static proof systems are algebraic or semi-algebraic, like the Nullstellensatz, Sherali-Adams and Sum-of-Squares proof systems. For these proof systems, extensions to proof systems for QBF were defined and studied by Beyersdorff et al. (SAT 2025). In this paper, we define and study an extension to a QBF proof system of the - to the best of our knowledge - only known pure Boolean static proof system, the hitting proof system. This proof system was introduced by Kullmann (Dagstuhl 2012) and first studied in detail by Filmus et al. (ITCS 2024).

ABSTRACT. For line-based propositional proof systems, there is a default way to extend them to proof system for quantified boolean formulas (QBF). For static proof systems, there is no such default method. Most known static proof systems are algebraic or semi-algebraic, like the Nullstellensatz, Sherali-Adams and Sum-of-Squares proof systems. For these proof systems, extensions to proof systems for QBF were defined and studied by Beyersdorff et al. (SAT 2025). In this paper, we define and study an extension to a QBF proof system of the - to the best of our knowledge - only known pure Boolean static proof system, the hitting proof system. This proof system was introduced by Kullmann (Dagstuhl 2012) and first studied in detail by Filmus et al. (ITCS 2024).