Mathematische Beweise per Routine

Constructor 0

Hallo.
Weiß jemand, ob es irgendwie möglich ist, ein Programm zu schreiben, welches unter Anwendung aller Ansätze eines geometrischen Beweises der aufgetragenen Problemstellung, selbständig eine Beweisführung durchführen kann.

henselstep

theoretisch ist es möglich, sogar jeden mathematischen Satz vom Computer beweisen zu lassen. Dir muss dann aber klar sein, dass wenn das System n Axiome hat, der Rechner na k Schritten n^k Sätze ausspuckt. Also ist so eine Idee nicht sinnvoll.

henselstep schrieb:

theoretisch ist es möglich, sogar jeden mathematischen Satz vom Computer beweisen zu lassen.

Nein es ist nichtmal theoretisch möglich JEDEN Satz zu beweisen. (Gödel Unvollständigkeitssatz)

Ansonsten Zustimmung. Ist ein hoffnungsloses Unterfangen und selbst die besten Programme können nicht mit einem Erstsemester mithalten.

Ich hätte gerne mal zumindest einen Satz gesehen, den ein Computerprogramm beweisen kann.
Vielleicht kann man mithilfe eines Programmes ein Resultat erzeugen, dass einen Gegenbeweis bildet - aber sonst ...

Schönes Beispiel hierzu:

1-2-3 1-5-9 1-8-6 1-4-7
4-5-6 4-8-3 4-2-9 2-5-8
7-8-9 7-2-6 7-5-3 3-6-9

Die Punkte 1 bis 9 bilden eine affine Ebene der Ordnung 3.
Die Geraden in dieser Ebene sind alle angegebenen Tripel (z.B. 1-2-3).
4-5-6 ist eine Parallele zu 1-2-3.
Wie man sieht, ist jeder Punkt mit jedem anderen auf genau einer Geraden verbunden. (Anwendungsbeispiel: Spielplan Volleyballligen! - je 3 spielen in einer Halle ihre drei Partien untereinander aus, an jedem Spieltag sind alle Teams beschäftigt, jeder kommt genau einmal gegen jeden anderen).

Das geht auch mit der Ordnung 4, und 5, aber mit 6 (36 Punkte, je 6 auf einer Geraden) geht es nicht. Keine Ebene möglich. 7 geht wieder und 8 und 9 .... wußte man seinerzeit noch nichts drüber (weiß nicht, wie's heute aussieht).
Aber man nahm an: 6 = 23, mehrere Primzahlen - ist vielleicht der Grund.
8 = 2^3 und 9 = 3^2 könnte gehen, 10 = 25 wieder nicht.
Ich habe damals das Problem auf eine Matrix mit diversen Bedingungen reduziert und konnte mit einem BruteForce-Algorithmus die Lösung finden.
8 und 9 existieren - 6 fand er nicht - 10 und 12 (3*2*2) auch nicht.
Aber - durch die Reduktion ist es nicht auszuschliessen, dass 10 nicht doch existiert. Man weiss *nur* - 8 und 9 gibt es. Hilft nicht sehr viel weiter...
(denn bei höheren Ordnungen schießt die Rechenzeit derart nach oben, dass man *etwas* auf das Resultat warten kann). Ob diese reduzierte Matrix die ganze Problematik einschränkt oder nicht - das findet kein Rechner (und ich auch nicht).

Ist wie mit einem Schachprogramm, dass ausrechnen könnte, wie's ausgeht. Das ist problemlos machbar (mit allen Endlichkeitsregeln im Schach, okay, manche sind turniergebunden...), läuft aber ewig und drei Tage.

lookias

hallo

http://www.cinderella.de/tiki-index.php

schau mal hier, das programm kann geometrische beweise fuehren.

Jester

Für den Vierfarbensatz gibt es bis jetzt afaik nur einen Beweis der größtenteils mit Hilfe des Computers geführt wurde, da die aufwändige Arbeit durch einen Menschen garnicht erledigt werden kann. Man streitet sich aber, ob das denn nun ein richtiger Beweis ist, oder nicht wenn man ihn als Mensch nicht nachvollziehen kann.

MfG Jester

Ich quote da mal unerlaubterweise:

"The theorem proving feature of Cinderella might turn out to be a bit controversial. To quote from the documentation, "Cinderella" does not use symbolic methods to create a formal proof, but a technique called 'Randomized Theorem Checking.'" If a statement is true for very many sufficiently general examples, does that tell us it is probably true in general? Some people will be sufficiently convinced to accept the statement and move on to something else. Others may use the highly probable truth of a statement as a guide to what to try to prove. Still others will not want to trust the technique at all. The question of the validity and utility of such "proofs" could enliven quite a few faculty lounges at coffee break. It might also generate useful discussions with students."

Das hat für mich nichts mit Beweisführung zu tun.
Divisionen funktionieren auch mit fast allen Werten...

henselstep

space schrieb:

henselstep schrieb:

theoretisch ist es möglich, sogar jeden mathematischen Satz vom Computer beweisen zu lassen.

Nein es ist nichtmal theoretisch möglich JEDEN Satz zu beweisen. (Gödel Unvollständigkeitssatz)

Ansonsten Zustimmung. Ist ein hoffnungsloses Unterfangen und selbst die besten Programme können nicht mit einem Erstsemester mithalten.

Hast recht. Ich meinte auch jeden beweisbaren Satz.

also man kann nicht nur jeden satz der euklidischen geometrie automatisch beweisen, sondern es wurden auch schon programme geschrieben, die das tatsächlich durchführen.

so ein programm kann man zb leicht in der programmiersprache prolog schreiben. ein solches programm ist bestimmt nicht länger als ein paar seiten.

die sache mit dem gödelschen unvollständigkeitssatz ist zwar schon richtig, gilt aber erst für axiomensysteme ab einer bestimmten komplexität (prädikatenlogik 2. stufe und höher). die axiome der euklidischen geometrie lassen sich aber bereits mit der prädikatenlogik 1. stufe ausdrücken. ein problem heißt unvollständigkeit, wenn es nicht möglich ist das problem it einer endlichen zahl von axiomen zu beschreiben. in diesem falle ist es UBERHAUPT NICHT möglich jede wahre aussage zu beweisen. weder durch einen computer noch durch einen noch so genialen menschen!

aber auch wenn das problem "vollständig" ist, dh der gödelsche unvollständigkeitssatz noch nicht gilt, so besteht immer noch das problem der "entscheidbarkeit". dh gibst du einen richtigen satz ein, dann wird das programm irgendwann tatsächlich erkennen, daß der satz richtig ist. gibst du jedoch einen falschen satz ein, dann wird das programm unter umständen ewig rechnen und nie erkennen, daß der satz falsch ist. wenn du also diesem programm einen satz eingibst von dem du nicht weißt, ob er richtig oder falsch ist, mußt du damit rechnen, daß das programm niemals eine lösung findet. das nennt man das "entscheidungsproblem".

die euklidische gemometrie ist zwar vollständig, aber nicht entscheidbar.

das ist jetzt alles etwas vereinfacht dargestellt aber im wesentlichen läufts darauf hinaus.