Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus (Q1869616)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 1902326
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus |
scientific article; zbMATH DE number 1902326 |
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
0.7887700200080872
0 references
0.753912627696991
0 references
0.7404405474662781
0 references
