Single Axioms for Boolean Algebra

June 2000

This page is a supplement to a report of the same name. Here is the current draft of the report. The report has pseudo links to Otter input files and other data files, and this web page, which echoes the structure of the paper, has the corresponding real links.

1. Introduction

2. Single Axioms via Pixley Terms

• schema-1a.in, schema-1a.proof
• schema-1b.in, schema-1b.proof

3. A Single Axiom for Sheffer Stroke

• pixley-2.in, pixley-2.out
• lengths.lisp

4. Shorter Single Axioms for Sheffer Stroke

• pixley-sheffer-shorter.in
• pixley-sheffer-30

4.1. Using Different Bases

• veroff2-hints.in, veroff2-hints.proof
• mccune.in, mccune.proof

4.2. A Schema for Two Absorption Equations

• schema-2-candidates.in
• schema-2-head
• schema-2-candidates
• schema-2a.in, schema-2a.proof
• schema-2b.in, schema-2b.proof
• sheffer-185.in
• sheffer-185-sound.in, sheffer-185-sound.proof
• sheffer-185-complete.in, sheffer-185-complete.proof

4.3. Taking Advantage of the Pixley Properties

• sheffer-head
• 60-sheffer-base-candidates
• 41-pixley-sheffer-bases
• pixley-sheffer-base.in, pixley-sheffer-base.proof
• sheffer-generate.in
• sheffer-105-sound.in, sheffer-105-sound.proof
• sheffer-105-complete.in, sheffer-105-complete.proof

5. Single Axioms with Standard Operators

5.1. Disjunction and Negation

• dn-generate.in
• dn-131-sound.in, dn-131-sound.proof
• dn-131-complete.in, dn-131-complete.proof

5.2. Disjunction, Conjunction, and Negation

• cdn-generate.in
• cdn-111-sound.in, cdn-111-sound.proof
• cdn-111-complete.in, cdn-111-complete.proof

5.3. Disjunction, Conjunction, Negation, 0, and 1

• cdn01-generate.in
• cdn01-127-sound.in, cdn01-127-sound.proof
• cdn01-127-complete.in, cdn01-127-complete.proof

6. Related Work

7. Further Work