Single Axioms for Boolean Algebra

TitleSingle Axioms for Boolean Algebra
Publication TypeReport
Year of Publication2000
AuthorsMcCune, W
Date Published06/2000
Other NumbersANL/MCS-TM-243

Explicit single axioms are presented for Boolean algebra in terms of (1) the Sheffer stroke; (2)disjunction and negation; (3) disjunction, conjunction, and negation; and (4) disjunction, conjunction, negation, 0, and 1. It was previously known that single axioms exist for these systems, but the procedures to generate them are exponential, producing huge equations. Automated deduction techniques were applied to find axioms of lengths 105, 131, 111, and 127, respectively, each with six variables.