Preprint:
Sam Buss and Ramyaa
"Short Refutations for the Equivalence-Chain Principle
for Constant-Depth Formulas"
Mathematical Logic Quarterly 64, 6 (2018) 505-513.
Download preprint.
Software: C++ software FmlaChain generates CNF formulations of the principles discussed in this paper.
Abstract: We consider tautologies expressing equivalence-chain properties in the spirit of Thapen and Krajicek, which are candidates for exponentially separating depth k and depth k+1 Frege proof systems. We formulate a special case where the initial member of the equivalence chain is fully specified and the equivalence-chain implications are actually equivalences. This special case is shown to lead to polynomial size resolution refutations. Thus it cannot be used for separating depth k and depth k+1 propositional systems. We state some Hastad switching lemma conditions that restrict the possible propositional proofs in more general situations.