Seite 1 von 1

Reduzierte Anforderung bei "Praktische Übung 2"

Verfasst: 27. Nov 2008 19:06
von aderhold
Offenbar gestaltet sich der Beweis des Lemmas delete deletes bei "ungeschickt" gewählten Hilfslemmas aufwendiger als erwartet. Um die Bearbeitungszeit für die Praktische Übung nicht ausufern zu lassen, reduzieren wir die Anforderung für ein erfolgreiches Testat folgendermaßen:

Das Lemma delete deletes muss nicht vollständig bewiesen sein, um das Testat zu bekommen. Es muss jedoch ein sinnvoller Beweisansatz vorliegen. Dies bedeutet konkret: Wenn man den Beweis mit "Verify" startet, enthält der Goalterm (mindestens) vier Teilaussagen ("maximal eingerückte boolesche Teilterme"). Mindestens eine dieser Teilaussagen muss bewiesen werden. Grob gesagt betreffen die Teilaussagen folgende Fälle:
  • Es wird nichts im linken Teilbaum gefunden.
  • Es wird nichts im rechten Teilbaum gefunden.
  • Beim Suchen in "add.left(t, dest)" wird man in "t" fündig.
  • Beim Suchen in "add.left(t, dest)" wird man in "dest" fündig.

Re: Reduzierte Anforderung bei "Praktische Übung 2"

Verfasst: 28. Nov 2008 17:15
von Steven
Gibt es irgendwelche gesonderten Gratifikationen für einen vollständigen Beweis von "delete deletes"?

Re: Reduzierte Anforderung bei "Praktische Übung 2"

Verfasst: 28. Nov 2008 17:57
von Langbaeh
hmm also bis jetzt konnte ich zwar delete deletes beweisen aber nicht deletes keeps ordered ^^

// edit hab inzwischen alles bewiesen ^^

Re: Reduzierte Anforderung bei "Praktische Übung 2"

Verfasst: 29. Nov 2008 18:36
von Jan Schejbal
Zunächst einmal - VIELEN DANK dass hier tatsächlich auf die Kritik reagiert wurde und die Anforderungen angepasst wurden. Das Praktikum war extremst zeitfressend (sogar mit dieser Erleichterung wäre es das, würde ich mal behaupten). Wirklich toll wäre es, wenn bei der nächsten Aufgabe von vorne herein bedacht würde, dass wir Studenten den Umgang mit VF erst lernen und noch nicht jahrelange Erfahrung damit haben und deswegen auch für erfahrene Nutzer trivial aussehende Schritte sehr lange dauern können.

Müssen wir die ca. 40 Lemmata tatsächlich topologisch sortiert auflisten? Das dürfte nämlich nochmal in eine ziemliche Arbeit ausarten, oder gibt es dafür nen Trick?

Re: Reduzierte Anforderung bei "Praktische Übung 2"

Verfasst: 29. Nov 2008 18:55
von Christoph-D
Jan Schejbal hat geschrieben:Müssen wir die ca. 40 Lemmata tatsächlich topologisch sortiert auflisten? Das dürfte nämlich nochmal in eine ziemliche Arbeit ausarten, oder gibt es dafür nen Trick?
Das ist keine verbindliche Aussage, aber IMHO solltet ihr die Lemmata in die korrekte Relation mit den vorgegebenen Lemmata setzen.

Wenn ihr also 10 Hilfslemmata für "delete keeps ordered.tree" habt, dann wäre die Reihenfolge dieser 10 Lemmata unter sich relativ egal, wichtig wäre aber, dass alle diese 10 Lemmata *über* "delete keeps ordered.tree" aber *unter* "insert inserts" stehen.

So eine "schwache Ordnung" lässt sich ziemlich schnell erreichen, wenn man im "Program Viewer" unter "used by" schaut, welches der vorgegebenen Lemmata dort steht.

Re: Reduzierte Anforderung bei "Praktische Übung 2"

Verfasst: 29. Nov 2008 22:30
von Christoph Walther
Jan Schejbal hat geschrieben:Wirklich toll wäre es, wenn bei der nächsten Aufgabe von vorne herein bedacht würde, dass wir Studenten den Umgang mit VF erst lernen und noch nicht jahrelange Erfahrung damit haben und deswegen auch für erfahrene Nutzer trivial aussehende Schritte sehr lange dauern können.
Das versuchen wir schon von vornherein, nur haben wir den schwierigkeitsgrad für die studenten bei dieser aufgabe leider falsch eingeschätzt.

cw.

Re: Reduzierte Anforderung bei "Praktische Übung 2"

Verfasst: 1. Dez 2008 16:43
von Fl4sh
Also die Aufgabe war auch mit herabgesetzten Anforderungen ziemlich knackig. Aber letztendlich haben wirs dann doch geschafft.
Ich habe nur Angst, dass so eine "Fehleinschätzung" dann auch in der Klausur passiert. :(

Re: Reduzierte Anforderung bei "Praktische Übung 2"

Verfasst: 1. Dez 2008 21:21
von Christoph Walther
Fl4sh hat geschrieben:Ich habe nur Angst, dass so eine "Fehleinschätzung" dann auch in der Klausur passiert. :(
Sowas kann man auch bei aller sorgfalt nie ausschließen, aber bei der bewertung der klausuren würde das dann schon berücksichtigt.

cw.