Verständliche halb-automatische Beweise

• Antragsteller: Professor Tobias Nipkow, Ph.D.
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 1998 bis 2003
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5102236

In der Fortsetzung dieses Vorhabens soll zunächst der Autor formaler Beweistexte durch weitergehende Konzepte der Isar Entwicklungsumgebung systematisch unterstützt werden. Ferner soll anstelle der bisher rein am Schriftsatz orientierten Präsentation ein allgemeines Modell für Dokumente mit formal-logischen Inhalten inklusive Beweisen treten; dies eröffnet eine weitere Perspektive der Integration von Isar mit anderen Systemen. Als typisches Anwendungsszenario der Gesamtumgebung soll ferner ein Beispiel zur Theorie objekt-orientierter Programmiersprachen in einer didaktish verwertbaren Form umgesetzt werden.

• DFG-Verfahren: Sachbeihilfen