Reduzierte Anforderung bei "Praktische Übung 2"

[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.

[Steven]

Gibt es irgendwelche gesonderten Gratifikationen für einen vollständigen Beweis von "delete deletes"?

[Langbaeh]

hmm also bis jetzt konnte ich zwar delete deletes beweisen aber nicht deletes keeps ordered ^^

// edit hab inzwischen alles bewiesen ^^

[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?

[Christoph-D]

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.

[Christoph Walther]

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.

[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.

[Christoph Walther]

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.