Diese Arbeit entstand für das Seminar Rechnerischer Gehalt von Beweisen. In dieser Arbeit wird der Satz, dass injektive Abbildungen von endlichen Mengen {1,...,n} auf sich selbst surjektiv sind, in mehreren Versionen geführt. Ziel dieser Arbeit ist der Beweis der Aussage in Minlog, einem in Scheme geschriebenes Programm zur Beweisführung. Außerdem wird aus dem Beweis ein Programm extrahiert, welches das Urbild von Funktionswerten berechnen kann.
Entwicklung eines Beweises in Minlog
Published on