---
title: "Computer-Aided Studies of All Possible Shortest Single Axioms for the Equivalential Calculus"
authors:
  - "John A. Kalman"
  - "J. G. Peterson"
doi: ""
url: "https://ijcai.org/proceedings/1983/220"
pdf: "https://ijcai.org/proceedings/1983/0220.pdf"
venue: "Proceedings of the Eighth International Joint Conference on Artificial Intelligence"
year: 1983
pages: "933-934"
track: "Theorem Proving"
keywords:
---

# Computer-Aided Studies of All Possible Shortest Single Axioms for the Equivalential Calculus

John A. Kalman, J. G. Peterson

*Proceedings of the Eighth International Joint Conference on Artificial Intelligence*, pages 933-934.

## Abstract

It has been known since 1939 that for a formula to be a single axiom for the equivalential calculus its length must be at least II, and that single axioms of this length exist. Also, a single axiom of length II must have the two-property. There are 630 formulas with the two-property and of length II. With computer assistance, the authors have shown that 612 of these 630 formulas are not single axioms. The main object of this paper is to outline the methods used to obtain these results. This paper logically precedes a recent paper of L. Wos which announces computer-assisted proofs that a further 5 of the 630 formulas are not single axioms, and should serve as an introduction to the method of schemata mentioned in that paper.