Verständliche halb-automatische Beweise

• Applicant: Professor Tobias Nipkow, Ph.D.
• Subject Area: Theoretical Computer Science
• Term: from 1998 to 2003
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants