Incredible Proof Machine
In den R\xe4umen des Entropia e.V. traf sich Joachim Breitner mit Sebastian Ritterbusch, um ihm von Computerbeweisen und der Incredible Proof Machine (http://incredible.pm/) zu erz\xe4hlen. Diese hatte er mit Unterst\xfctzung von Kollegen und Freunden f\xfcr einen dreit\xe4gigen Workshop im Oktober 2015 am Science College J\xfclich mit Sch\xfclerinnen und Sch\xfclern im Start-Stipendium f\xfcr motivierte und neu zugewanderte Jugendliche in Mittel- und Oberstufe unter Unterst\xfctzung der Deutsche Telekom Stiftung entworfen. Der mathematische Beweis ist grundlegender Bestandteil der Mathematik und die Technik des Beweisen wird im Mathematik- oder Informatikstudium vielfach ge\xfcbt, wie es auch im Modell036 Podcast zur Analysis beschrieben wurde. Dennoch wird das wichtige Thema nur selten in der Schule angesprochen, da korrekte Beweise sehr formal und abstrakt sind. Mit einem spielerischen Zugang wird der Einstieg in die exakte Beweistheorie f\xfcr Sch\xfcler und Mathematik-Interessierte nicht nur m\xf6glich, sondern erm\xf6glicht auch neue Formen der Lehre wie den Modell051 Flipped Classroom. Beweise gehen von bestehenden Aussagen und festgelegten Axiomen aus, um neue Aussagen oder Erkenntnisse zu belegen. Von der Aussage "es regnet" kann man beispielsweise mit einem fiktiven Axiom "wenn es regnet, werden Stra\xdfen nass" schlie\xdfen, dass gilt: "die Stra\xdfe ist nass". Und man kann daraus mit der Technik des Widerspruch-Beweis zeigen, dass aus der Aussage "die Stra\xdfe ist trocken" folgt, dass "es regnet nicht" gilt. Denn (und das ist der Beweis), w\xfcrde es regnen, so w\xe4re die Stra\xdfe nass, also nicht trocken. Wann ist aber nun ein Beweis richtig? Diese Frage kann sich jeder selbst beantworten, in dem man einen vorliegenden Beweis versucht nachzuvollziehen. Eine Alternative ist die Beweispr\xfcfung mit dem Computer, wie beispielsweise mit Isabelle. Diese Art von Software richtet sich allerdings in erster Linie an fortgeschrittene Nutzer und setzt Kentnisse in sowohl in der Logik als auch in der (funktionalen) Programmierung voraus, und so suchte Joachim nach einer einfachereren Methode, beweisen zu lernen und die Ergebnisse maschinell zu pr\xfcfen. Mit der von ihm kreierten Incredible Proof Machine werden Beweise durch Ziehen und Setzen bildlich erstellt, in der Form eines Graphen. So wird das Beweisen zu einem Puzzle-Spiel mit Erfolgserlebnis, das man nach und nach l\xf6sen kann, ohne dabei die exakte Mathematik zu verlassen. In dem Spiel gibt es viele Aufgaben, die zu l\xf6sen sind. In der \xdcbersicht sind diese in Lektionen geordnet und zeigen jeweils durch einen breiten Strich, dem Inferenzstrich getrennt, von welchen Aussagen oben man welche Aussagen unten beweisen soll. W\xe4hlt man eine Aufgabe aus, so sieht man die gegebenen Aussagen, die oberhalb des Striches waren, als Quellen auf einem Arbeitsblatt. Die zu beweisenden Aussagen erscheinen als Senken. Von den Quellen kann man nun per Maus Verbindungen zu den Senken ziehen- entweder direkt, oder mit Hilfe zus\xe4tzlicher Bl\xf6cke, bzw. gegebener Beweisregeln, aus einer Toolbox links, die ebenfalls zur Verf\xfcgung stehen und weitere gegebene Axiome darstellen. Sind alle offenen Senken bewiesen, so leuchtet unten eine Zeile gr\xfcn auf, als Best\xe4tigung f\xfcr einen geschafften Level- eine positive Best\xe4rkung, die nicht ganz so spektakul\xe4r ist, wie bei Populous. W\xe4hrend man auf dem Arbeitsblatt spielt, gibt die Incredible Proof Machine unmittelbar R\xfcckmeldung, falls eine Verbindung so keinen Sinn macht: Will man die Aussage B mit Aussage A beweisen, so wird die Linie zwischen den beiden sofort rot, und gibt dem Spielenden die Hilfestellung, wo mindestens ein Fehler steckt. Die logischen Aussagen und die gegebenen Beweisregeln verwenden eine g\xe4ngige Notation zur Beschreibung logischer Verkn\xfcpfungen. Ein \u2228 (sieht wie der kleine Buchstabe v aus), steht f\xfcr die logische Oder-Verkn\xfcpfung und die Notation stammt vom lateinischen Wort vel. Das umgekehrte Symbol \u2227 steht f\xfcr die logische Und-Verkn\xfcpfung. ...