automatisches Überprüfen von Beweisen |
| 17.10.2018, 21:32 | TomS | Auf diesen Beitrag antworten » | ||||||||
| automatisches Überprüfen von Beweisen Angenommen, wir haben einen mathematischen Ausdruck, von dem behauptet wird, dass es sich um den Beweis eines Theorems handelt. Ist es dann möglich, für jeden beliebigen derartigen Ausdruck in endlicher Zeit zu prüfen - d.h. zu beweisen oder zu widerlegen - ob ein korrekter Beweis vorliegt? Ist dies - je Axiomensystems - mittels eines generischen Algorithmus (Proof Checkers) möglich? Ich denke dabei an soetwas wie Metamath. Ich sehe zwei Probleme: Zum ersten ist es evtl. möglich, dies wiederum mittels eines Diagonalverfahrens auszuhebeln. Zum zweiten sehe ich die Problematik, dass man die Korrektheit des Proof Checker ebenfalls beweisen müsste, was zunächst mal überhaupt eines Beweises oder einer beweisbar korrekten Konstruktion bedarf (wiederum die bekannte Anfälligkeit), oder eines zweiten Proof Checkers, um den Beweis zur Korrektheit des ersten zu prüfen (infiniter Regess). Letzteres entfiele im Falle eines generischen Proof Checkers, da dieser prinzipiell in der Lage wäre, die Korrektheit seines eigenen Beweises prüfen. |
||||||||||
| 17.10.2018, 22:25 | Elvis | Auf diesen Beitrag antworten » | ||||||||
Ein Beweis ist eine bestimmte Zeichenfolge, die auch wieder eine Aussage ist. Nach Goedel ist nicht jede wahre Aussage beweisbar, also auch nicht jeder korrekte Beweis entscheidbar. Wenn ich mich nicht irre, kann man keine Beweismaschine bauen, weil das Halteproblem für Turingmaschinen nicht lösbar ist. |
||||||||||
| 17.10.2018, 22:51 | TomS | Auf diesen Beitrag antworten » | ||||||||
Die Schlussfolgerung in dem „also“ ist mir zu schnell. Eine Theorem T folgt mittels eines Beweises B aus Axiomen A. D.h. in etwa B = „A => ... => T“ Für eine Beweismaschine sind A und T gegeben, B gesucht.
Ja. Aber im vorliegenden Fall geht es lediglich daraum, dass jedes „=>“ logisch korrekt ist. Man muss nichts finden, nur die logische Zulässigkeit prüfen. Ich sage nicht, dass das immer funktioniert, aber es klingt leichter, als den Beweis zu finden. |
||||||||||
| 18.10.2018, 07:57 | Elvis | Auf diesen Beitrag antworten » | ||||||||
Du hast recht, und ich habe keine Antwort. |
||||||||||
| 19.10.2018, 11:42 | TomS | Auf diesen Beitrag antworten » | ||||||||
Hast du eine Idee, wie man hier weiterkommt? Nach Recherche finde ich zu "proof checker" nichts, immer nur "proof assistant", und das ich nicht das, was ich suche. Teilweise liest es sich so, wie wenn die Korrektheit und Vollständigkeit von Proof Checkern unproblematisch wäre, aber eine präzise Aussage finde ich nicht. |
||||||||||
| 19.10.2018, 12:05 | Elvis | Auf diesen Beitrag antworten » | ||||||||
Wenn jemand einen proof checker verkaufen möchte wird er nicht verraten, wo seine Grenzen liegen, er wird immer nur Werbung für seine Vorzüge machen. Meine Studienzeit liegt lange zurück, und ich habe leider viel aus der Theorie der Berechenbarkeit und Turingmaschinen vergessen. Ob ein "was auch immer" automatisierbar ist, hängt jedenfalls mit diesen Begriffen zusammen. |
||||||||||
| Anzeige | ||||||||||
|
|
||||||||||
| 19.10.2018, 13:50 | Huggy | Auf diesen Beitrag antworten » | ||||||||
Wo sollte da das Problem liegen? Das Problem der maschinellen Beweisprüfung liegt darin, einen in üblicher mathematischer Form vorliegenden Beweis erst mal in eine für einen Proof Checker lesbare Form zu bringen. In dieser Form besteht der Beweis aus einer Folge von Symbolketten. Der Proofchecker muss nun überprüfen, ob sich all diese Symbolketten durch ein gegebenes endliches System von Erzeugungsregeln aus den schon vorher erzeigten Symbolketten erzeugen lassen. Durch die Axiome des betrachteten Axiomensystems lassen sich einige Symbolketten aus der leeren Menge von Symbolketten erzeugen. Das verwendete Logiksystem enthält die Regeln, nach denen aus schon erzeugten Symbolketten neue erzeugt werden können. Diese Beweisprüfung unterscheidet sich grundsätzlich von der Problematik der maschinellen Beweiserzeugung, also von der Problematik des Halteproblems. Natürlich muss auch bei einem Proof Checker überprüft werden, ob in ihm die zulässigen Umformungsregeln korrekt implementiert sind. Das kann letztendlich nur ein Mensch machen, weil dieser ja auch die Umformungsregeln vorgibt. Noch ein interessanter Artikel dazu: http://www.spiegel.de/wissenschaft/mensc...-a-1222123.html |
||||||||||
| 19.10.2018, 15:07 | TomS | Auf diesen Beitrag antworten » | ||||||||
Ich nehme an, dass dies bereits erfolgt sein
Ich hatte das anders verstanden, aber wahrscheinlich ist das irrelevant. Die Axiome und die Logik definieren das von dir genannte System S von Erzeugungsregeln. Gegeben sei eine Symbolkette T. Ich starte mit einer Symbolkette A. Der Proof Checker muss überprüfen, ob T mittels S aus A generierbar ist. Dabei ist der Beweis "A => ... T" in kleine Stücke zerlegt, idealerweise muss der Proof Checker nur sehr elementare Schritte nachvollziehen. Ich kann ihm jedenfalls nicht nur die Axiome sowie das Resultat T geben und ihn alle Schritte konstruieren lassen; das wäre ja kein proof checking sondern proof generation (und das führt zum Halteproblem). Richtig?
Klar.
Die Frage ist, ob das nicht auf einen infiniten Regress hinausläuft. Wenn das nicht der Fall sein soll, dann müsste der Proof Checker so einfach gehalten sein, dass er nicht anfällig für das Halteproblem ist. |
||||||||||
| 19.10.2018, 15:09 | TomS | Auf diesen Beitrag antworten » | ||||||||
Danke für den Link; den kannte ich schon. Kennst du eine etwas detaillierter Quelle? |
||||||||||
| 19.10.2018, 15:53 | Huggy | Auf diesen Beitrag antworten » | ||||||||
Richtig. Der Proof Checker darf nur eine endliche und nach oben abschätzbare Menge von Prüfungen vornehmen müssen, damit man nicht in das Halteproblem hineinläuft.
Ja und nein. Der Proof Checker ist ein Programm. Irgendjemand muss feststellen, ob das Programm das tut, was es tun soll. Das kann man ganz oder teilweise wieder einem anderen Programm überlassen, womit das Problem aber nur verlagert ist. Der unendliche Regress lässt sich nur vermeiden, wenn man glaubt, dass es Programme gibt, deren Korrektheit der Mensch überprüfen kann. Ich dachte, einen etwas ausführlicheren Artikel in Spektrum der Wissenschaft in Erinnerung zu haben, konnte ihn aber nicht finden. So einen richtig griffigen Übersichtsartikel kenne ich auch nicht, obwohl mich diese Thematik auch interessiert. Einen weiteren Einblick gibt vielleicht: http://scienceblogs.de/mathlog/2018/10/1...-der-geometrie/ |
||||||||||
| 19.10.2018, 22:45 | Toms | Auf diesen Beitrag antworten » | ||||||||
Danke, dann sind wir uns da einig.
Ich denke, man muss zwei Fälle unterscheiden. Die Frage, ob ein Beweis der Korrektheit prinzipiell möglich oder unmöglich ist, sowie die Frage, ob Beweise praktisch Fehler enthalten können, und wie man dies feststellt oder ausschließt.
Der Mensch kann das auch nicht besser als ein Algorithmus. Ich will auf folgendes hinaus: (1) es gibt Axiomensysteme, in denen Gödels Unvollständigkeitssätze gelten (2) es gibt aber auch solche, in denen sie nicht gelten, d.h. die beweisbar konsistent sind, oder in denen - beweisbar - alle wahren Sätze auch beweisbar sind u.u. Die spannende Frage ist, ob es Axiomensysteme (1) gibt, für für die beweisbar Proof Checker existieren, die für beliebige Sätze in (1) nicht anfällig sind für das Halteproblem. D.h. dass zumindest für alle vorgelegten Beweisanssätze sicher in endlicher Zeit entschieden werden kann, sie korrekt sind oder nicht. |
||||||||||
|
|
Verwandte Themen
| Die Beliebtesten » |
|
| Die Größten » |
|
| Die Neuesten » |
