Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus (Q1869616): Difference between revisions
From MaRDI portal
Removed claim: reviewed by (P1447): Item:Q583186 |
Set OpenAlex properties. |
||
(3 intermediate revisions by 3 users not shown) | |||
Property / reviewed by | |||
Property / reviewed by: N. K. Zamov / rank | |||
Normal rank | |||
Property / describes a project that uses | |||
Property / describes a project that uses: OTTER / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1023/a:1021693818601 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1620994827 / rank | |||
Normal rank |
Latest revision as of 10:12, 30 July 2024
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