Praktikum 2

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

Praktikum 2

Beitrag von Gnomix »

Kann jemand einen Hinweis geben, wie man am besten anfängt.
Meine Ansätze laufen nämlich immer wieder ins Leere.

robert.n
Nerd
Nerd
Beiträge: 673
Registriert: 29. Sep 2008 19:17

Re: Praktikum 2

Beitrag von robert.n »

Du möchtest meistens irgendeine Eigenschaft von irgendeinem Objekt beweisen.

Beispiel: ordered, unique, ...

Jetzt werden aber allerlei Operationen mit dem jeweiligen Objekt durchgeführt (im Beweisbaum). Das beste ist, wenn du Lemmas formulierst, die zeigen, dass die jeweilige Eigenschaft durch diese Operationen nicht zerstört wird, sondern aufrecht erhalten bleibt.
Die Operationen, die du dabei berücksichtigen musst, werden ziemlich sicher irgendwo im Beweisbaum auch mal auftauchen.

Beispiel: 2 Listen werden aneinandergehängt

Oder mal konkret auf das P2 bezogen: Wie verhält sich die Breite eines Codes, wenn man ihn umdreht?

Code: Alles auswählen

Formal: aus was folgt width-of-each-is-n(reverse(c), n) ?

mit c : list[code], n : nat
Ich meine mich erinnern zu können, dass das irgendwo im Beweisbaum mal so ähnlich vorkam bzw. gebraucht wurde.

Wenn du herausfinden willst ob ein Lemma tatsächlich gebraucht wird, dann kannst du mit Insert Hypothese oder Case Analysis die jeweilige Behauptung einfach einfügen und schauen, wie es weitergeht. Manchmal sieht man dann sofort, dass wirklich nur noch dieses eine Lemma gebraucht wird.

MfG, Robert

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

Re: Praktikum 2

Beitrag von bashFish »

Watt fuer Ansaetze hast du denn?

Wir hatten doch schonmal festgestellt, dass man so net weiterkommt :?

http://d120.de/forum/viewtopic.php?f=182&t=17230 / Sprechstunde

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

Re: Praktikum 2

Beitrag von Gnomix »

Nun ich habe bisher versucht per Generate Lemma ein paar Hilfslemmas zu erzeugen, die mir das Verifizieren vereinfachen.
Dies hat aber nur bedingt geholfen, denn nur ein Lemma konnte ich damit und mit Generalisierung beweisen.

Ich denke ich muss einfach nochmal neu anfangen und ohne diese Injektiv/Kommutativ und so arbeiten.
Ich habe dies eigentlich auch erstmal nur gemacht um einen eindruck zu bekommen, wie die Methoden arbeiten.

Dann habe ich mir die bisherigen Hilfestellungen durchgelesen und überlegt, dass man irgendwie zeigen muss, dass sich durch prepend und so nur wenig ändert.
Bei Prepend z.B. die Länge nur um eins zunimmt.
nun muss ich nur noch schauen, wie ich das so aufschreibe.

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

Re: Praktikum 2

Beitrag von Gnomix »

Juchu, die 2.1 und 2.2, sowie die 2.3a haben wir fertig bekommen.

Nun hänge ich an der 2.3b.
Die Aussage unique(generate-gray-code(n)) kann er irgendwie nicht beweisen obwohl ich nachweise, dass prepend die Eigenschaft unique erhält.
Für <> und reverse schaffe ich es nicht.

Benutzeravatar
DerInformator
Mausschubser
Mausschubser
Beiträge: 98
Registriert: 24. Okt 2008 13:02
Wohnort: DA

Re: Praktikum 2

Beitrag von DerInformator »

Gnomix hat geschrieben:Juchu, die 2.1 und 2.2, sowie die 2.3a haben wir fertig bekommen..
2.1 und 2.2 hab ich auch...
aber wie hast du denn 2.3 gemacht? O.o (diese Frage ist natürlich rethorisch ^^)

Das einzige Lemma, dass ich mir erstellt habe und grün ist, ist nicht sinnvoll (wenn k unique dann tl(k) unique xD )
Ansonsten gehe ich so vor wie in der Aufgabenstellung (prunen an der wurzel und manuelle induktion)
Aber dann klappts irgendwie nicht. Versuche elementare Sachen über prepend und <> und ob diese unique erhalten oder nicht zu beweisen...aber irgendwie fehlen mir anscheinend noch 100 lemmas :S
"Do not go where the path may lead, go instead where there is no path & leave a trail"

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

Re: Praktikum 2

Beitrag von bashFish »

fuer <> gilt es allgemein ja auch nicht ~ nur weil du eines dieser lemmas gebrauchen konntest, heisst das nicht, dass du auch alle weiteren mutationen davon formulieren kannst/sollst/musst!
Mit dem Programm arbeiten -> schau dir den Beweisbaum an und finde heraus, was genau du fuer <> Eigenschaften brauchst!

[ Vlt solltest du erst Lemmas definieren, die dann mit use-Lemma anwenden, und dann erst das Beweisen anfangen (bzw so weitermachen)! ]

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

Re: Praktikum 2

Beitrag von bashFish »

Gnomix hat geschrieben:
Ansonsten gehe ich so vor wie in der Aufgabenstellung (prunen an der wurzel und manuelle induktion)
Aber dann klappts irgendwie nicht. Versuche elementare Sachen über prepend und <> und ob diese unique erhalten oder nicht zu beweisen...aber irgendwie fehlen mir anscheinend noch 100 lemmas :S
der Teil mit der Induktion galt eigentlich nur bei der a und war eine gegebene Vereinfachung~ (wenn man die Heuristik entscheiden laesst, kommen 3 Teilbaeume raus ~)

Auch bei dir: Die Lemmas aus dem Beweisbaum Generalisieren/ Erahnen und nicht randomisiert raten!

(und ja , es koennen einige Lemmas gebraucht werden , bis man gefundene Lemmas beweisen kann!)

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

Re: Praktikum 2

Beitrag von Gnomix »

Bei 2.3a habe ich erstmal die Schritte gemacht, die auf dem Aufgabenblatt stehen.
Danach habe ich zwei Teilbäume erhalten, die nicht bewiesen werden konnten.
Nun habe ich diese einmal per Generate und einmal per manuellem Generalisieren gelöst.

Bei der 2.3b, komme ich aber immer noch nicht wirklich voran.
Mein Goalterm lautet:

Code: Alles auswählen

if{?⁺(⁻(n)),
  if{unique(create-gray-code(⁻(n))),
    unique(
     prepend(zero, create-gray-code(⁻(n)))
     <> prepend(one, reverse(create-gray-code(⁻(n))))),
    true},
  true}
Für Prepend(bit, list

Code: Alles auswählen

) konnte ich ein Lemma bauen, aber sobald reverse hinzu kommt klappt es nicht.
Das Hilfslemma aus der a verwendet er überhaupt nicht.

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Praktikum 2

Beitrag von Nathan Wasser »

Gnomix hat geschrieben: Bei der 2.3b, komme ich aber immer noch nicht wirklich voran.
Mein Goalterm lautet:

Code: Alles auswählen

if{?⁺(⁻(n)),
  if{unique(create-gray-code(⁻(n))),
    unique(
     prepend(zero, create-gray-code(⁻(n)))
     <> prepend(one, reverse(create-gray-code(⁻(n))))),
    true},
  true}
Für Prepend(bit, list

Code: Alles auswählen

) konnte ich ein Lemma bauen, aber sobald reverse hinzu kommt klappt es nicht.
Das Hilfslemma aus der a verwendet er überhaupt nicht.[/quote]

Generell gilt: Wenn die geschachtelte Induktion fehlschlägt => [b]wegschneiden![/b] (mitsamt move und delete hypotheses)

In diesem Fall ist es zwar relativ egal, aber im Allgemeinen kann nach "Delete Hypotheses" ein Beweis unmöglich werden. Deshalb sollte man diese Teilbäume wegschneiden, wenn sie nicht sofort zum Ziel führen.

Das Hilfslemma aus der (a) wird automatisch verwendet, wenn man die anderen notwendigen Lemmata bewiesen hat. Um herauszufinden welche Lemmata noch fehlen, kann man aber das Hilfslemma auch per Hand mit "Use Lemma" anwenden.

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

Re: Praktikum 2

Beitrag von Gnomix »

Ich begreife es einfach nicht.
Jedesmal wenn ich versuche etwas zu beweisen, komme ich immer wieder auf mein schon geposteten Goalterm oder Verschachtelungen.
Ich denke mittlerweile ich brauche eine Aussage in der Art, wenn der Graycode mit n Stellen unique ist, dann auch der mit n+1.
Aber das kann Verifun nicht beweisen, auch wenn ich für prepend, <> und reverse es bewiesen habe.

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Praktikum 2

Beitrag von Nathan Wasser »


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

Re: Praktikum 2

Beitrag von Gnomix »

Was ich einfach nicht verstehe ist, dass wenn ich das Hilfslemma aus der a anwende er direkt wieder vereinfacht zur ursprünglichen Aussage.

Das heißt doch quasi er braucht/nutzt das Lemma nicht.

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Praktikum 2

Beitrag von Nathan Wasser »

Nicht unbedingt. Es könnte auch bedeuten, dass VeriFun den Goalterm nicht mit dem Lemma vereinfachen kann, weil andere Lemmata fehlen.

In diesem Fall aber vermute ich, dass eine nicht-hilfreiche Substitution bei der Benutzung des Hilfslemmas angegeben wird.

Die Poolsprechstunden sind vermutlich der beste Ort so etwas zu klären.

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

Re: Praktikum 2

Beitrag von Gnomix »

Einer meiner Gruppenmitglieder hat es hinbekommen, indem er die Lemmas manuell angewendet hat.

Antworten

Zurück zu „Archiv“