Verifun Methodiken

bashFish
Mausschubser
Mausschubser
Beiträge: 77
Registriert: 3. Okt 2007 17:38

Verifun Methodiken

Beitrag von bashFish »

Vlt. koennten sich ja die Verifun-Gequaelten dazu ermuntern lassen, eine Art "Best-Practices" zu schreiben (oder in Form von Beitraegen in diesem Topic zu sammeln), die man untereinander kommunizieren und vlt sogar ans naechste Semester weitergeben kann?
Euer Vorgehen zu einem Erfolgserlebnis ist hier wuenschenswert!

Ein Ansatz in mehreren Formen : http://d120.de/forum/viewtopic.php?f=18 ... 42#p105342 + 2 folgende Beitraege


(!! Bitte keine konkreten Loesungen dokumentieren :/ )
Zuletzt geändert von bashFish am 5. Nov 2009 12:50, insgesamt 1-mal geändert.

Steven
Kernelcompilierer
Kernelcompilierer
Beiträge: 425
Registriert: 2. Sep 2008 10:00
Wohnort: Frankfurt am Main

Re: Verifun Methodiken

Beitrag von Steven »

Das Problem dabei ist, dass es keinen allgemein hilfreichen Weg gibt. Du musst dir immer das aktuelle Beweisziel ansehen und dann entscheiden, wie du vorgehst. Generell gibt es zwei Möglichkeiten:
  • Du kannst unter Annahme der Hypothesen (H) und Induktionshypothesen (IH), zeigen, dass das Goal gilt, also eine Implikation A und IH => Goal zeigen.
  • Du kannst zeigen, dass deine Hypothesen und Induktionshypothesen einen Widerspruch aufweisen. Damit wird die Prämisse der oben genannten Implikation falsch und die Konklusion ist unerheblich.
Welche Möglichkeit du wählst, hängt vom Einzelfall ab.

Einfach mal "ins Blaue" Lemmas raten ist eine miese Idee, allerdings sammelt sich im Laufe der Verifun-Benutzung eine gewisse Menge recht allgemeiner Lemmata an (z.B. Kommutativität von plus, Reflexivität von kleinergleich usw.). Diese kannst du sammeln und probeweise in eine neue Aufgabenstellungs-Datei importieren, in der Hoffnung, dass Verifun damit schon ein paar Dinge vereinfachen kann. Aber Achtung: Manchmal schießt die Heurisitik von Verifun auch über das Ziel hinaus, d.h. sie wendet Lemmas an, die an der aktuellen Stelle nutzlos sind oder die Aussage sogar verkomplizieren. Wenn du mit der "Library-Methode" arbeitest, musst du explizit auf solche Fälle achten und sie im Zweifelsfall wieder prunen.

Der nächste Tipp ist auch wieder keine Patentlösung: Wenn du eine Reihe verschachtelter if-Abfragen mit recht großen then- und else-Teilen hast, kannst du diese in zwei Beweisknoten aufteilen, indem du die if-Bedingung als Hypothese annimmst. Der erste Knoten bekommt dann die positive Hypothese (d.h. wir zeigen das Ziel unter der Annahme, die Hypothese sei korrekt, was genau dem then-Teil entspricht), der zweite Knoten bekommt die negierte Hypothese (d.h. wir zeigen das Ziel unter der Annahme, die Hypothese sei falsch, was genau dem else-Teil entspricht). Das macht das Beweisziel oft übersichtlicher, du hast dann aber auch mehr Hypothesen und mehr Beweisknoten. Schlimmstenfalls war die Aufteilung inhaltlich nutzlos, d.h. du machst in beiden Teilknoten die gleichen Aktionen und hast somit doppelte Arbeit.

Wenn du ein neues Lemma schreibst und dir nicht sicher bist, ob das überhaupt nützlich ist, macht es Sinn, im ursprünglichen Beweis zuerst eine manuelle Lemma-Anwendung zu versuchen, um zu sehen, ob sich das gewünschte Ergebnis einstellt. Wenn nicht, überarbeitest du dein Lemma. Damit verschwendest du keine Zeit auf Lemmata die zu nichts führen. Aber auch das ist nur eine Heuristik: Vielleicht bringt dir das Lemma nur zusammen mit anderen ebenfalls noch fehlenden Lemmata etwas und du siehst das nicht direkt. Insbesondere ist die Aussage nicht umkehrbar: Selbst wenn dein Ursprungsbeweis mit deinem neuen Lemma direkt aufgeht und gelb wird, heißt das nicht, dass dein Lemma korrekt ist!!!

Im Endeffekt läuft es also darauf hinaus, dass du dir eine Arbeitstechnik suchst, wie du aus den Informationen der Beweisknoten (Goal, Hypothesen, Induktionshypothesen) die Aussage extrahierst und damit auf einen Beweisansatz schließt.

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Re: Verifun Methodiken

Beitrag von Gnomix »

Es ist auch sehr hilfreich verschiedene Versionen zu speichern.
Sprich ihr habt eine Teilaufgabe gelöst, dann sichert erstmal eure arbeit.

Denn leider kommt es immer wieder vor, dass Verifun bei einem Beweis/Falsifikation hängen bleibt und nicht mehr zu einem Ende kommt,
dann könnt ihr nicht mehr speichern.

Außerdem könnt ihr so schnell einen "alten" Stand öffnen und könnt euren Beweis von vorne beginnen, falls ihr euch mal verrannt habt.

bashFish
Mausschubser
Mausschubser
Beiträge: 77
Registriert: 3. Okt 2007 17:38

Re: Verifun Methodiken

Beitrag von bashFish »

Denn leider kommt es immer wieder vor, dass Verifun bei einem Beweis/Falsifikation hängen bleibt und nicht mehr zu einem Ende kommt,
dann könnt ihr nicht mehr speichern.
Du hast jederzeit die "Proof Control" offen! Dort kannst du im Reiter ganz links die aktuellen Aktionen einsehen. Wenn du auf eine Aktion rechts-klickst, kannst du durch Cancel die komplette Aktion abbrechen. Brichst du die 1. ab, wird der Beweis abgebrochen und nurnoch mit Syntax Pruefung usw. abgebrochen.


Aber ja, guter Punkt, ich wuerde auch raten, oefters unter (aussagekraeftigen?) Namen zu speichern! Besonders, bevor man ein "prune" versucht! Erwartet nicht, dass nach jedem Doppelklick der gleiche Beweisbaum herauskommt! Besonders, wenn ihr eine Generalisierung schreibt, solltet ihr mit Use Lemma oder Apply Equation das Lemma an die Stelle bringen, wo es gefordert wird, und nicht hoffen, dass er schon selbst alles richtig macht, wenn man den Beweis nochmal neu startet!

Antworten

Zurück zu „Archiv“