Studienprojekt

Beweis von formalen Aussagen mit Hilfe eines Theorembeweisers

In diesem Projekt sollen formale Aussagen über Haskell-Programme mithilfe eines Theorem­beweisers wie Coq automatisiert bewiesen werden. Der Nutzer eines Theorem­beweisers 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 Theorem­beweiser sich am besten eignet, um Aussagen über Programme mithilfe von gleichungs­basierten 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.

Zurück