Praktische Übung 1.1 (d), Lemma bleibt blau

[M.Schanz]

Ich tue mich noch ein bisschen schwer mit VeriFun. Ist es denn richtig, dass man VeriFun erstmal versuchen lässt das Lemma zu beweisen und dann wenn es nicht mehr von alleine weiterkommt unter "Proof" -> "Refute" ein Gegenbeispiel angibt?

Und wenn ja: Ist es dann richtig dass das Lemma im "Program" Panel (linke Seite) blau bleibt und nicht rot wird (siehe Bild)?

[Christoph Walther]

Ist es dann richtig dass das Lemma im "Program" Panel (linke Seite) blau bleibt und nicht rot wird (siehe Bild)?

Die antwort steht auf folie 3/45. Und vergleichen Sie einmal Ihren screenshot mit dem auf folie 3/46. Und noch ein tipp: Sie sollten sich die folien zu einem thema gründlich anschauen, bevor Sie mit dem system arbeiten. Das spart Ihnen (und anderen) viel zeit beim lösen der aufgaben.

[M.Schanz]

Nach nochmaligem lesen der Folien und Neubearbeitung der Aufgabe habe ich habe jetzt den Beweisbaum an dem Knoten "Delete Hypotheses" abgeschnitten und anschließend "Proof\Refute" gewählt. Ich denke das ist richtig so?! Es kommt mir trotzdem etwas komisch vor, da mit Program\Disprove Lemma automatisch ein Gegenbeispiel gefunden wird (und dieser Schritt nicht mehr Rückgängig gemacht werden kann => Also muss die Aufgabe neu geladen werden um es 'korrekt' zu machen)

[dschneid]

Nach nochmaligem lesen der Folien und Neubearbeitung der Aufgabe habe ich habe jetzt den Beweisbaum an dem Knoten "Delete Hypotheses" abgeschnitten und anschließend "Proof\Refute" gewählt. Ich denke das ist richtig so?! Es kommt mir trotzdem etwas komisch vor, da mit Program\Disprove Lemma automatisch ein Gegenbeispiel gefunden wird (und dieser Schritt nicht mehr Rückgängig gemacht werden kann => Also muss die Aufgabe neu geladen werden um es 'korrekt' zu machen)

Natürlich kannst du "Disprove Lemma" rückgängig machen: Das tut ja nichts anderes, als automatisch ein Gegenbeispiel für "Refute" zu finden. Aber den so entstandenen Refute-Knoten im Beweisbaum kannst du genauso prunen wie alle anderen.

Prinzipiell kannst du auch direkt auf den Wurzelknoten des Beweisbaumes "Refute" anwenden, du musst nicht erst einen Beweisversuch laufen lassen und dann irgendwo weit unten ansetzen. Es kann aber eben passieren, dass das Goal an der Wurzel noch zu kompliziert ist, als dass ein Gegenbeispiel gefunden werden könnte. Das ist hier aber nicht so.