Tautologies over implication with negative literals

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.

• Type: Journal
• Year: 2010
• Where: MLQ
• Authors: Hervé Fournier, Danièle Gardy, Antoine Genitrini, Marek Zaionc
• Keywords: Logical Expressions, MLQ 2010, Opposite Literals, Single Binary Connector