Flyspeck II: the basic linear programs
Flyspeck II: the basic linear programs
复制标题
DOI：
10.1007/s10472-009-9168-z
复制
发表时间：
2009-08
影响因子：
1.2
通讯作者：
Steven Obua;T. Nipkow
中科院分区：
文献类型：
--
作者：
Steven Obua;T. Nipkow
本文是Flyspeck项目的第二个主要贡献，该项目的目标是完整的机器验证形式化的开普勒猜想的证明，托马斯黑尔斯在1998年。我们指定，生成和绑定黑尔斯松散地称之为基本的线性规划。我们在交互式证明助手Isabelle中实现了这一点。这项工作有两个主要方面：逻辑推理和可信计算。当然，可信计算可以被认为是逻辑推理的一种特殊情况，但关于计算速度的要求需要特殊处理。我们的解决方案是HOL计算库。这项工作的很大一部分致力于这个库的设计和实现。然后，我们应用该库表明，92.5%的所有驯服的图给提高基本的线性规划是不一致的。Übersetzte Kurzfassung：Diese Arbeit ist der zweite größere Beitrag zum Flyspeck-Projekt，dessen Ziel die vollständige maschinelle Verifikation des Beweises der Keplerschen Vermutung ist，den托马斯黑尔斯1998 gegeben hat.我们将为哈雷斯的项目提供专门的、通用的和特殊的服务，并将为伊莎贝尔提供内部援助。第二个方面是：物流运输和物流服务。Natürlich kann verlässliches Rechnen als Spezialfall von logischem Schließen angesehen韦尔登aber Anforderungen an die Rechengeschwindigkeit verlangen nach einer gesonderten Lösung.我们将为您提供一个完整的程序包。我们的工作是设计和实现这些程序包。据我们所知，有92.5%阿勒石墨烯元件生产线计划不一致。
This thesis is the second major contribution to the Flyspeck project which has as its goal the complete machine-verified formalization of the proof of the Kepler conjecture that Thomas Hales has given in 1998. We specify, generate and bound what Hales loosely calls the basic linear programs. We do this within the interactive proof assistant Isabelle. There are two major aspects of this work: Logical reasoning and trusted computing. Of course trusted computing can be considered as a special case of logical reasoning but requirements regarding the speed of computing demand a special treatment. Our solution to this problem is the HOL Computing Library. A substantial part of this work is dedicated to the design and implementation of this library. We then apply the library to show that 92.5% of all tame graphs give raise to basic linear programs which are inconsistent.Übersetzte Kurzfassung: Diese Arbeit ist der zweite größere Beitrag zum Flyspeck-Projekt, dessen Ziel die vollständige maschinelle Verifikation des Beweises der Keplerschen Vermutung ist, den Thomas Hales 1998 gegeben hat. Wir spezifizieren, generieren, und berechnen Schranken für die von Hales sogenannten elementaren linearen Programme, und zwar innerhalb des interaktiven Beweisassistenten Isabelle. Zwei Aspekte sind dabei prägend: Logisches Schließen und verlässliches Rechnen. Natürlich kann verlässliches Rechnen als Spezialfall von logischem Schließen angesehen werden aber Anforderungen an die Rechengeschwindigkeit verlangen nach einer gesonderten Lösung. Als solche stellen wir ein Programmpaket für verlässliches Rechnen vor. Ein beträchtlicher Teil unserer Arbeit ist dem Design und der Implementierung dieses Programmpakets gewidmet. Mit seiner Hilfe beweisen wir, dass 92, 5% aller zahmen Graphen elementare lineare Programme induzieren, die inconsistent sind.