Ziemlich überraschend sind Bernd Gräfrath und Silvio Baier auf ein Problem mit dem Prüfprogramm für Beweispartien Euclide gestoßen: Für eine Beweispartie findet Euclide keine Lösung, obgleich eine existiert, die auch von Natch gefunden wird.
Bernd stellt in einem Beitrag, den ihr hier herunterladen könnt, die Aufgabe vor — sie ist nicht nur wegen dieses Fehlers sehenswert!
Übrigens findet Euclide bei den angegebenen Vergleichsaufgaben die Lösungen. Ich persönlich vermute, dass eine Optimierung zu “scharf” geschaltet ist. Über die weitere Entwicklung werde ich jedenfalls gern berichten.
bernd und silvio: ich finde es gut, dass ihr eure aufgaben öffentlich gemacht (und damit vielleicht auf dem altar der aufklärungsarbeit geopfert) habt!
der computer, besser: ein programm prüft schachprobleme. aber wer prüft das programm?!
wer kann und mag überhaupt eine derartige prüfung durchführen (zeitaufwand, einschlägische kenntnisse)?
es bleibt dabei: solange ein programm nicht alle fälle durchspielt (natürlich nicht unbedingt im einzelnen; aber eine vollständige fallzerlegung muss vorliegen), bleibt ein restrisiko, das eigentlich nicht hingenommen werden kann, insbesondere bei beweispartien nicht.
ich erinnere mich aus meinen (mathematik-)studentenzeiten an ein eindrückliches buch mit dem titel “counterexamples in analysis” (link dazu: http://books.google.ch/books/about/Counterexamples_in_Analysis.html?id=cDAMh5n4lkkC&redir_esc=y). es enthält beispiele seltsamster funktionen mit “absurdesten” eigenschaften, die man mit “gesundem menschenverstand” nie für möglich halten würde. berühmtestes beispiel ist vielleicht eine funktion, die überall stetig, aber nirgends differenzierbar ist. eine solche hat bereits karl weierstraß gefunden und beschrieben.
ohne einen wirklichen beweis ist man nie sicher, dass nicht ganz unerwartetes passieren kann, gerade bei klassischen retros nicht.
es ist erstaunlich, dass der bug bei euclide an einem relativ kurzen und “von auge” gut überblickbaren beispiel zutage getreten ist, und dies erhöht natürlich auch das unbehagen.
ich bin gespannt, wie diese sache weitergeht, und ob derartige fragen auch bei anderen schachprogrammen auftreten werden. eine kritik an den zugehörigen programmieren zu üben, liegt mir ganz fern. ihr (wohl meist unbezahlter!) einsatz ist hoch zu schätzen, und ich hoffe sehr, dass sich die probleme lösen und klären lassen.
Lieber Urs, danke für Deinen verständnisvollen Kommentar. Mal sehen, ob Herausgeber und Preisrichter das Problem (in beiden Versionen) trotzdem am Informalturnier teilnehmen lassen!
Dein zweiter Kommentar spricht ein sehr tiefes Problem an: Es ist gar nicht so klar, was “C+” eigentlich bedeutet! Letztlich muß eben unser menschlicher Verstand das letzte Wort haben, wenn es um die Beurteilung geht, ob ein Computerprogramm korrekt arbeitet…
natürlich! klar!