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.