Einen Beweis für einen Algorithmus schreiben

Question

Hallo Leute, ich versuche, 2 Algorithmen zu vergleichen und dachte, ich könnte versuchen und einen Beweis für sie schreiben !!! (Meine Mathe saugt so daher die Frage)

Normalerweise in unserer Mathestunde im vergangenen Jahr hat uns eine Frage wie

beweist gegeben würden: (2r + 3) = n (n + 4)

dann ich würde die benötigten 4 Stufen tun und die Antwort am Ende

bekommen, wo ich stecken bin ist Prims und Kruskals beweisen - wie ich diese Algorithmen oben so in eine Form wie die mathmatical man bekommen kann ich

beweisen, gehen kann

hinweis: ich frage nicht menschen zu ans wer es für mich - mir helfen, es einfach in eine Form zu bekommen, wo ich ein mir

dank

gehen kann

Answer 1

Sie geben nicht viele Details, aber es ist eine Gemeinschaft der Mathematiker (mathematisches Wissensmanagement MKM) die Werkzeuge entwickelt haben, um Computerbeweise für Mathematik zu unterstützen. Siehe zum Beispiel:

http://imps.mcmaster.ca/

und die neueste Konferenz

http://www.orcca.on.ca/conferences/cicm09/mkm09/

Answer 2

Aus meiner Mathematikunterricht an der Uni I (vage) erinnern Prims und Kruskals Algorithmen beweisen - und Sie nicht angreifen es durch Schreiben in einer mathematischen Form. Stattdessen nehmen Sie bewährte Theorien für Graphen und kombinieren sie z. http://en.wikipedia.org/wiki/Prim%27s_algorithm#Proof_of_correctness um den Beweis zu bauen.

Wenn Ihr auf der Suche, die Komplexität zu beweisen, dann einfach durch das Wirken des Algorithmus ist es O (n^2). Es gibt einige Optimierungen für den speziellen Fall, in dem der Graph spärlich ist, was dies auf O (nlogn) reduzieren kann.

Answer 3

Wo ich bin stecken ist Prims und Kruskals beweisen - wie kann ich diese Algorithmen in eine Form wie die mathmatical man erhalten oben, damit ich gehen kann

Ich glaube nicht, zu beweisen, können Sie direkt. Beweisen Sie stattdessen, dass beide eine MST generieren, und beweisen Sie, dass zwei beliebige MST gleich sind (oder äquivalent, da Sie für einige Graphen mehr als eine MST haben können). Wenn beide Algorithmen MSTs generieren, die sich als äquivalent erweisen, sind die Algorithmen äquivalent.

Answer 4

Um die Korrektheit eines Algorithmus zu beweisen, müssen Sie normalerweise (a) zeigen, dass es endet und (b) dass seine Ausgabe die Spezifikation dessen erfüllt, was Sie versuchen zu tun. Diese beiden Beweise werden sich ziemlich von den algebraischen Beweisen unterscheiden, die Sie in Ihrer Frage erwähnen. Das Schlüsselkonzept, das Sie benötigen, ist mathematical induction. (Es ist recursion für Beweise.)

Nehmen wir quicksort als Beispiel.

Um zu beweisen, dass quicksort endet immer, würden Sie zeigen zunächst, daß es für die Eingabe von Länge endet 1. (Diese trivialer Fall ist.), Dass dann zeigen, wenn es für die Eingabe von Länge bis zu n endet, dann wird es für die Eingabe von Länge beenden n + 1. Dank der Induktion dies ausreicht, um zu beweisen, dass der Algorithmus für alle Eingabe beendet.

Um zu beweisen, dass Quicksort korrekt ist, müssen Sie die Spezifikation der Vergleichssortierung in präzise mathematische Sprache konvertieren. Wir wollen, dass der Ausgang ein permutation des Eingangs zu sein, so dass, wenn i ≤ j dann ein _i ≤ ein _j. Der Beweis, dass die Ausgabe von Quicksort eine Permutation der Eingabe ist, ist einfach, da sie mit der Eingabe beginnt und nur Elemente vertauscht. Die zweite Eigenschaft zu beweisen, ist ein wenig komplizierter, aber wieder kann man Induktion verwenden.

Answer 5

In den meisten Fällen hängt der Nachweis von dem Problem ab, das Sie in der Hand haben. Einfache Argument kann manchmal ausreichen, zu anderen Zeiten könnten Sie benötigen strenge Beweis. Ich habe einmal eine Korollar und einen Beweis des bereits bewiesenen Satzes verwendet, um meinen Algorithmus zu rechtfertigen. Aber das ist für ein College-Projekt.

Answer 6

Vielleicht möchten Sie eine halbautomatische Proof-Methode ausprobieren. Nur um etwas anderes zu erreichen;) Wenn Sie zum Beispiel eine Java-Spezifikation von Prims und Kruskals Algorithmen haben, die optimal auf demselben Graphenmodell aufbauen, können Sie die KeY Prover verwenden, um die Äquivalenz des Algorithmus zu beweisen.

Der entscheidende Teil besteht darin, Ihre Beweispflicht in Dynamic Logic zu formalisieren (dies ist eine Erweiterung der Logik erster Ordnung mit Arten und Mitteln der symbolischen Ausführung von Java-Programmen). Die Formel zu beweisen, könnte die folgenden (skizzenhaft) Muster entspricht:

\forall Graph g. \exists Tree t. 
    (<{KRUSKAL_CODE_HERE}>resultVar1=t) <-> (<{PRIM_CODE_HERE}>resultVar2=t) 

Dies drückt aus, dass für alle Graphen, beide Algorithmen beenden und das Ergebnis ist der gleiche Baum.

Wenn Sie Glück haben und Ihre Formel (und Algorithmusimplementierungen) richtig sind, kann KeY es automatisch für Sie beweisen. Falls nicht, müssen Sie möglicherweise einige quantifizierte Variablen instanziieren, was es erforderlich macht, den vorherigen Beweisbaum zu untersuchen.

Nachdem Sie die Sache mit KeY bewiesen haben, können Sie entweder froh sein, etwas gelernt zu haben oder einen manuellen Beweis aus dem KeY-Beweis zu rekonstruieren - das kann eine langwierige Aufgabe sein, da KeY viele Java-spezifische Regeln kennt sind nicht leicht zu verstehen. Vielleicht können Sie jedoch etwas wie das Extrahieren einer Herbrand-Disjunktion aus den Begriffen ausführen, die KeY verwendet hat, um existenzielle Quantoren auf der rechten Seite von Sequenzen im Beweis zu instanziieren.

Nun, ich denke, dass KeY ist ein interessantes Tool und mehr Menschen gewöhnen sollten kritischen Java-Code mit Tool wie das beweisen;)