Aufgabenstellung im Rahmen eines Interdisziplinären Projekts
Zertifizierte Implementierung von Algorithmen aus der Computeralgebra
Aufgabenstellung im Rahmen eines Interdisziplinären Projekts
(Satz zur Motivation)
Für den Theorembeweiser Isabelle wird an der TU, in Zusammenarbeit mit Cambridge und Tokio, zur Zeit eine Bibliothek algebraischer Theorien entwickelt. In diesem Projekt übernehmen Sie eine konkrete Teilaufgabe, z. B. die Formalisierung von faktoriellen Ringen mit dem Ziel, in Isabelle zu zeigen, dass Polynome über einem faktoriellen Ring wieder einen faktoriellen Ring bilden. Die Themen bewegen sich im Bereich der Gruppen- und Ringtheorie.