战胜XCB问题--等价微积分最后最短单公理的方法论发现
Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus
摘要：
本文采用了有效的方法，详细回答了一个问题，这个问题在四分之一个世纪的时间里，尽管各种研究人员进行了深入的研究，但仍然是开放的。公式XCB = e（x，e（e（x，y），e（z，y）），z））在推理规则由分离（肯定前件）和替换组成时是经典等价演算的单一公理吗？当函数e表示等价时，这个演算可以用公式e（x，x），e（e（x，y），e（y，x））和e（e（x，y），e（e（y，z），e（x，z））很自然地公理化，它们分别对应于自反性、对称性和传递性。(We注意e（x，x）依赖于另外两个公理。至此，13个长度为11的经典等价的最短单公理已经被发现，而XCB是唯一剩下的长度为11的公式，其地位尚未确定。为了证明XCB确实是这样一个公理，我们集中在凝聚分离规则，一个规则，捕捉分离与适当的一般，但限制，形式的替代。我们在本文中提出的证明包括25个应用程序的凝聚分离，完成了推导的传递性，其次是推导的对称性。我们还讨论了一些因素，这些因素可能部分解释了为什么XCB如此长时间地拒绝放弃其宝藏。我们的方法依赖于自动推理程序OTTER应用的各种策略。这样就结束了对等价演算的最短单公理的搜索。
英文摘要：
With the inclusion of an effective methodology, this article answers in detail a question that, for a quarter of a century, remained open despite intense study by various researchers. Is the formula XCB = e(x,e(e(e(x,y),e(z,y)),z)) a single axiom for the classical equivalential calculus when the rules of inference consist of detachment (modus ponens) and substitution? Where the function e represents equivalence, this calculus can be axiomatized quite naturally with the formulas e(x,x), e(e(x,y),e(y,x)), and e(e(x,y),e(e(y,z),e(x,z))), which correspond to reflexivity, symmetry, and transitivity, respectively. (We note that e(x,x) is dependent on the other two axioms.) Heretofore, thirteen shortest single axioms for classical equivalence of length eleven had been discovered, and XCB was the only remaining formula of that length whose status was undetermined. To show that XCB is indeed such a single axiom, we focus on the rule of condensed detachment, a rule that captures detachment together with an appropriately general, but restricted, form of substitution. The proof we present in this paper consists of twenty-five applications of condensed detachment, completing with the deduction of transitivity followed by a deduction of symmetry. We also discuss some factors that may explain in part why XCB resisted relinquishing its treasure for so long. Our approach relied on diverse strategies applied by the automated reasoning program OTTER. Thus ends the search for shortest single axioms for the equivalential calculus.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
