Studienprojekt
Beweis von formalen Aussagen mit Hilfe eines Theorembeweisers
In diesem Projekt sollen formale Aussagen über Haskell-Programme mithilfe eines Theorembeweisers wie Coq automatisiert bewiesen werden. Der Nutzer eines Theorembeweisers gibt dabei lediglich vor, welche Schritte durchgeführt werden sollen, die Durchführung der einzelnen Schritte übernimmt der Beweiser. Somit erhält man eine sehr viel höhere Sicherheit der Korrektheit eines Beweises als bei einer manuellen Durchführung.
Im ersten Teil soll untersucht werden, welcher Theorembeweiser sich am besten eignet, um Aussagen über Programme mithilfe von gleichungsbasierten Umformungen zu beweisen. Im zweiten Teil sollen dann je nach Zeit ausgewählte Aussagen über Programme, z.B. bereits per Hand bewiesene Aussagen, automatisiert bewiesen werden.
Für dieses Projekt ist ein wenig Affinität für mathematische formale Aussagen wünschenswert, aber ansonsten sind keine weiteren Vorkenntnisse erforderlich.