Mathematical Logic Quarterly

Short refutations for an equivalence‐chain principle for constant‐depth formulas

Journal Article


We consider tautologies expressing equivalence‐chain properties in the spirit of Thapen and Krajíček, 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 Håstad switching lemma conditions that restrict the possible propositional proofs in more general situations.

Related Topics

Related Publications

Related Content

Site Footer


This website is provided by John Wiley & Sons Limited, The Atrium, Southern Gate, Chichester, West Sussex PO19 8SQ (Company No: 00641132, VAT No: 376766987)

Published features on are checked for statistical accuracy by a panel from the European Network for Business and Industrial Statistics (ENBIS)   to whom Wiley and express their gratitude. This panel are: Ron Kenett, David Steinberg, Shirley Coleman, Irena Ograjenšek, Fabrizio Ruggeri, Rainer Göb, Philippe Castagliola, Xavier Tort-Martorell, Bart De Ketelaere, Antonio Pievatolo, Martina Vandebroek, Lance Mitchell, Gilbert Saporta, Helmut Waldl and Stelios Psarakis.