Computer-Aided Studies of All Possible Shortest Single Axioms for the Equivalential Calculus
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 11, and that single axioms of this length exist. Also, a single axiom of length 11 must have the two-property. There are 630 formulas with the two-property and of length 11. 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.
Cite
Text
Kalman and Peterson. "Computer-Aided Studies of All Possible Shortest Single Axioms for the Equivalential Calculus." International Joint Conference on Artificial Intelligence, 1983.Markdown
[Kalman and Peterson. "Computer-Aided Studies of All Possible Shortest Single Axioms for the Equivalential Calculus." International Joint Conference on Artificial Intelligence, 1983.](https://mlanthology.org/ijcai/1983/kalman1983ijcai-computer/)BibTeX
@inproceedings{kalman1983ijcai-computer,
title = {{Computer-Aided Studies of All Possible Shortest Single Axioms for the Equivalential Calculus}},
author = {Kalman, John A. and Peterson, J. G.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1983},
pages = {933-935},
url = {https://mlanthology.org/ijcai/1983/kalman1983ijcai-computer/}
}