Proof Development with Ωmega: The Irrationality of \(\sqrt 2\)
Proof Development with Ωmega: The Irrationality of \(\sqrt 2\)
复制标题
Ωmega 的证明开发：(sqrt 2) 的非理性
DOI：
10.1007/978-94-017-0253-9_11
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Martin Pollet
中科院分区：
文献类型：
--
作者：
J. Siekmann;Christoph Benzmüller;Armin Fiedler;A. Meier;I. Normann;Martin Pollet
众所周知的定理认为\（\ sqrt 2 \）的非理性性是作为一个案例研究，以比较15个（互动）定理证明系统[Wiedijk，2002]。这代表了自动扣除领域中重点的重要转变，从过去的人造问题转向了真正的数学挑战。
The well-known theorem asserting the irrationality of \(\sqrt 2\) was proposed as a case study for a comparison of fifteen (interactive) theorem proving systems [Wiedijk, 2002]. This represents an important shift of emphasis in the field of automated deduction away from the somehow artificial problems of the past back to real mathematical challenges.