Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus (Q1869616)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus |
scientific article |
Statements
Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus (English)
0 references
28 April 2003
0 references
This paper answers the following question: Is the formula \(\text{XCB}= e(x,e(e(e(xy)\), \(e(z,y)),z))\) a single axiom for the classical equivalential calculus when the rules of inference consist of detachment and substitution? Heretofore, thirteen shortest single axioms for classical equivalence of length eleven have been discovered, and XCB was the only remaining formula whose status was undetermined. This result ends the search for shortest single axioms for the equivalential calculus.
0 references
equivalence
0 references
equivalential calculus
0 references
single axioms
0 references
shortest single axioms
0 references
detachment
0 references
condensed detachment
0 references
XCB
0 references
OTTER
0 references
automated reasoning
0 references