Praktikum 3.2b)

Benutzeravatar
mantra
Computerversteher
Computerversteher
Beiträge: 385
Registriert: 23. Okt 2005 23:56
Wohnort: Wiesbaden

Praktikum 3.2b)

Beitrag von mantra »

Hallo.
Beim Beweis von "\(\approx\) is transitive" bin ich an eine Stelle gestossen, an der sehr offensichtlich die Induktionshypothese steht, nur dass ein paar Argumente in anderer Reihenfolge stehen. Dass die Reihenfolge keine Rolle spielt, konnte ich mit einem Lemma zeigen, aber der Beweis kommt kein Stueck voran. Auch mit "Use Lemma" bleibt der alte Term stehen. VeriFun erkennt also nicht, dass es sich um die Induktionshypothese handelt. "Apply Equation" bietet mir bei meinem Umformungslemma keine Position an, auf die ich es anwenden koennte - was ist denn die Vorausseztung, um eine Gleichung anzuwenden?
Wie kann ich die (durch das Lemma bewiesenermassen korrekte) Umformung durchfuehren, damit da die Hypothese steht?

aderhold
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 212
Registriert: 21. Okt 2005 10:50

Re: Praktikum 3.2b)

Beitrag von aderhold »

Es kann passieren, dass VeriFun eine Use-Lemma-Anwendung durch eine anschließende Simplification "rückgängig" macht. Man kann in einem solchen Fall die Simplification nach dem Use Lemma abschneiden ("Prune") und von hier aus weiter arbeiten.

Voraussetzung für Apply Equation ist, dass die anzuwendende Gleichung L = R "syntaktisch passt". Es muss z. B. eine Substitution \(\sigma\) geben, so dass \(\sigma(L)\) im Goalterm vorkommt. Dieses Vorkommen kann dann durch \(\sigma(R)\) ersetzt werden.

In deinem Fall kann es also sein, dass du den Goalterm durch deine "Reihenfolge-ist-egal"-Lemmas erst in eine Form bringen musst, um die gewünschte Gleichung anwenden zu können. Wenn diese Lemmas allerdings nicht mit Apply Equation anwendbar sind, könnte es sein, dass ihre syntaktische Struktur nicht zum Goalterm passt. Um das zu prüfen, lass dir mal mit der "Show all braces"-Checkbox im Program Viewer und Proof Viewer die genaue Klammerstruktur anzeigen. Vielleicht ist der Unterschied hier zu finden.

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

Re: Praktikum 3.2b)

Beitrag von Christoph Walther »

aderhold hat geschrieben:Um das zu prüfen, lass dir mal mit der "Show all braces"-Checkbox im Program Viewer und Proof Viewer die genaue Klammerstruktur anzeigen.
Die klammerstruktur erkennt man auch, indem man mit der maus auf einen term zeigt.

Benutzeravatar
mantra
Computerversteher
Computerversteher
Beiträge: 385
Registriert: 23. Okt 2005 23:56
Wohnort: Wiesbaden

Beitrag von mantra »

Jetzt geht es :) Mein Fehler war, dass ich in der Liste "Available Equations" nicht noch die Untereintraege des Lemmas ausgewaehlt habe. Erst zwei Ebenen tiefer wurde mir die Position angeboten - dann wurde die Gleichung ohne Murren angewandt und der Induktionsschritt klappte.

Die Klammerstruktur konnte ich allerdings nur durch "Show all braces" ansehen.

Gibt es eigentlich die Moeglichkeit, Lemmata im nachhinein in der Verzeichnisstruktur zu verschieben, ohne sie zu duplizieren? Waere ganz gut, wenn ich nachtraeglich etwas Struktur hineinbekommen wuerde ;)

Penny
Neuling
Neuling
Beiträge: 4
Registriert: 11. Mär 2005 18:57

Beitrag von Penny »

Ja du kannst sie verschieben. Einfach per Drag and Drop :-)

Benutzeravatar
mantra
Computerversteher
Computerversteher
Beiträge: 385
Registriert: 23. Okt 2005 23:56
Wohnort: Wiesbaden

Beitrag von mantra »

Interessant :D .. Pool-Rechner gewechselt - und schon gehts! Dafffuer klemmen hier ein paar Tasten

Antworten

Zurück zu „Archiv“