Praktikum 1

nobody
Windoof-User
Windoof-User
Beiträge: 36
Registriert: 26. Okt 2009 11:58

Praktikum 1

Beitrag von nobody »

sers,
ich hänge gerade an aufgabe 1.3 c fest. hat die schon jemand gelöst? falls ja, wie viele hilfslemmata sind denn nötig?

Benutzeravatar
igor.a
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 143
Registriert: 28. Sep 2009 16:05

Re: Praktikum 1

Beitrag von igor.a »

Hab 2 Lemmata dafür gebraucht..

1.3d) ist dann leider noch komplexer =(

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Praktikum 1

Beitrag von mister_tt »

Aus eigener Erfahrung: Es macht nicht wirklich Sinn, die Anzahl der Lemmata zu vergleichen... Damit macht ihr euch nur Stress und beschränkt eure Ideen!

Viele Wege führen zum Beweis eines Lemmas...

nobody
Windoof-User
Windoof-User
Beiträge: 36
Registriert: 26. Okt 2009 11:58

Re: Praktikum 1

Beitrag von nobody »

igor.a hat geschrieben:Hab 2 Lemmata dafür gebraucht..

1.3d) ist dann leider noch komplexer =(
... oder anders gefragt: in welche richtung gehen denn die lemmata? müssen eher allgemeine aussagen getroffen werden oder müssen sie sich auf die in dieser teilaufgabe eingeführten funktionen beziehen?

lg

d_noack
Neuling
Neuling
Beiträge: 2
Registriert: 19. Mär 2009 15:21

Re: Praktikum 1

Beitrag von d_noack »

Die Richtung deiner Lemmata ergibt sich aus dem Beweisbaum den du bisher hast. Kann Verifun mit den aktuellen Aussagen den Beweis nicht schließen, fallen dir sicherlich einige wiederkehrende Aussagen im Beweisbaum auf, die vielleicht leicht, aber nicht wesentlich verändert/vereinfacht werden können. An diesen Stellen solltest du im Zweifelsfall ansetzen und überlegen, welche (allgemeinen) Aussagen du über die hier verwendeten Operatoren und Funktionen treffen kannst, mit denen Verifun dann evtl. weiter arbeiten kann. Das können/müssen auch ganz "triviale" Aussagen sein, die für dich vielleicht selbstverständlich sind.

Deine ersten Ansätze müssen auch gar nichts zwangsweise direkt mit der Lösung zu tun haben. Manchmal verändert aber ein scheinbar unpassendes Lemma den Beweisbaum auf eine Art, dass dir auf einmal klar wird, wo du ansetzen musst.

Benutzeravatar
JanM
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 157
Registriert: 24. Aug 2010 10:58

Re: Praktikum 1

Beitrag von JanM »

kann ich bei verifun auch so tun als ob ein lemma bereits bewiesen wäre und dann damit ein anderes lemma beweisen.
beispiel: ich habe ein lemma, das ich beweisen wil. dann definiere ich mir ein hilfslemma, für dessen beweis ich allerdings ein weiteres lemma benötigen würde. Kann ich dann irgendwie angeben, dass das hilfslemma gilt um zu prüfem dass sich die mühe lohnt ein weiteres lemma zu finden?

mister_tt
Kernelcompilierer
Kernelcompilierer
Beiträge: 502
Registriert: 29. Sep 2008 15:54

Re: Praktikum 1

Beitrag von mister_tt »

Du kannst "so tun als ob ein Lemma bewiesen wäre", ja. Dafür musst du das Lemma am entsprechenden Knoten jedoch manuell anwenden ("Use Lemma"). Kann damit der Beweis vervollständigt werden, wird der entsprechende Knoten gelb statt grün. Das bedeutet, dass das Lemma bewiesen ist, sobald das angewandte Hilfslemma bewiesen ist.

Antworten

Zurück zu „Archiv“