Computer-Aided Studies of All Possible Shortest Single Axioms for the Equivalential Calculus
Proceedings of the Eighth International Joint Conference on Artificial Intelligence. Theorem Proving. 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.
@inproceedings{ijcai1983p220,
title = {Computer-Aided Studies of All Possible Shortest Single Axioms for the Equivalential Calculus},
author = {Kalman, John A. and Peterson, J. G.},
booktitle = {Proceedings of the Eighth International Joint Conference on
Artificial Intelligence, {IJCAI-83}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Alan Bundy},
pages = {933--934},
year = {1983},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1983/220},
}
TY - CPAPER TI - Computer-Aided Studies of All Possible Shortest Single Axioms for the Equivalential Calculus AU - Kalman, John A. AU - Peterson, J. G. T2 - Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83 PB - International Joint Conferences on Artificial Intelligence PY - 1983 SP - 933 EP - 934 UR - https://ijcai.org/proceedings/1983/220 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
