Ziele und Anwendungen

Viele interessante Mengen M von Objekten sind dadurch charakterisiert, dass ein Objekt O genau dann zu M gehört, wenn ein zu O gehöriges Beweis-objekt B existiert. Oft ist leicht zu verifizieren, dass B zu O gehört, aber B selbst ist schwer zu finden. Klassische Beispiele aus der Berechenbarkeits-und Komplexitätstheorie sind ein drei-färbarer Graph, sowie eine Drei-Färbung, oder eine PCP-Instanz mit einem Lösungswort.
Wir hatten im Rahmen des Praktikums Funktionale Programmierung die Aufgabe, autotool-Module zur Verwaltung solcher Objekte und Beweise zu entwerfen und zu implementieren.
Insbesondere soll ein Wettbeweb ermöglicht werden, bei dem die Teilnehmer sich gegenseitig Aufgaben stellen. Man sendet ein passendes Paar (O,B) ein, das vom System geprüft wird. Daraufhin wird O (ohne B) veröffentlich, und die anderen Studenten müssen selbst dazu passende B finden. Nach bestimmten Kriterien werden Wertungspunkte auf Aufgabensteller und -löser verteilt.

Ziel ist die Erstellung eines interaktiven Moduls für das bestehende automatische Korrekturprogramm autotool.
Es soll dem Studenten des Grundstudiums die Möglichkeit gegeben werden, selbst Aufgaben und deren Lösungen einzusenden.