Hast du schon einmal einen mathematischen Beweis in einem logischen Kalkül geführt? In einer formalen Sprache also, die nur bestimmte fundamentale Beweisschritte zulässt? Ein Beweis von selbst „trivialen“ Aussagen kann da schnell recht lang werden!
Für das Seminar „Rechnerischer Gehalt von Beweisen“ habe ich einen solchen Beweis in Minlog geschrieben. Minlog ist ein in der Programmiersprache Scheme geschriebenes Beisführungsprogramm und wird maßgeblich an der LMU entwickelt. Die von mir bewiesene Aussage lautete: Jede injektive Abbildung der Menge {1,2..n} in sich selbst ist surjektiv. Auch wenn diese Aussage einfach erscheint, ich musste über 600 Code-Zeilen dafür schreiben!
Aber wo liegt der Vorteil in einer solch umständliches Beweisführung? Ein Vorteil ist, dass in Minlog geführte Beweise weiterverwendet werden können. So konnte ich aus meinem Beweis automatisch ein Programm extrahieren, welches Urbilder einer injektiven Abbildung {1..n} in sich selbst ermittelt. Aber schau dir doch die PDF zu meiner Arbeit an ;-)
