Praktische Übung 1.1 (d), Lemma bleibt blau

M.Schanz
Mausschubser
Mausschubser
Beiträge: 45
Registriert: 19. Okt 2010 19:44

Praktische Übung 1.1 (d), Lemma bleibt blau

Beitrag von 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)?
Bild

Christoph Walther
Dozentin/Dozent
Beiträge: 86
Registriert: 1. Nov 2005 18:51

Re: Praktische Übung 1.1 (d), Lemma bleibt blau

Beitrag von Christoph Walther »

M.Schanz hat geschrieben: 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
Mausschubser
Mausschubser
Beiträge: 45
Registriert: 19. Okt 2010 19:44

Re: Praktische Übung 1.1 (d), Lemma bleibt blau

Beitrag von 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
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Praktische Übung 1.1 (d), Lemma bleibt blau

Beitrag von dschneid »

M.Schanz hat geschrieben: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.

Antworten

Zurück zu „Archiv“