Tautologies over implication with negative literals
Hervé Fournier, Danièle Gardy, Antoine Genitrini, Marek Zaionc · Mathematical logic quarterly · 2010
Abstract We consider logical expressions built on the single binary connector of implication and a finite number of literals (Boolean variables and their negations). We prove that asymptotically, when the number of variables becomes large, all tautologies have the following simple structure: either a premise equal to the goal, or two premises which are opposite literals (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)