Abstract in English

The basic motivation of this work is to make formal theory developments with machine-checked proofs accessible to a broader audience. Our particular approach is centered around the Isar formal proof language that is intended to support adequate composition of proof documents that are suitable for human consumption. Such primary proofs written in Isar may be both checked by the machine and read by human-beings; final presentation merely involves trivial pretty printing of the sources. Sound logical foundations of Isar are achieved by interpretation within the generic Natural Deduction framework of Isabelle, reducing all high-level reasoning steps to primitive inferences.

Diese Arbeit möchte maschinelle Beweise einem breiteren Publikum zugänglich machen. Die hierzu eingeführte formale Sprache Isar erlaubt, Beweis - Dokumente auf einem für menschliche Leser angemessenen Niveau zu verfassen. Die logische Fundierung erfolgt durch Interpretation als abstrakte Inferenzen im Isabelle System. Die Isabelle/Isar Umgebung ist generisch bezüglich Objekt-Logiken und Beweiswerkzeugen, und unterstützt gleichermaßen Natürliches Schließen sowie algebraische Umformungen. Anwendungen aus der Logik, Mathematik und Informatik belegen die Vielseitigkeit und Praxistauglichkeit der Isar Konzepte.