Praktikum 3

treo
Windoof-User
Windoof-User
Beiträge: 31
Registriert: 3. Okt 2007 21:58

Praktikum 3

Beitrag von treo »

Ich bedanke mich dafür das diesmal daran gedacht wurde das FGI3 eine 4 SWS Veranstaltung ist.
Der Aufwand war diesmal eine Größenordnung weniger.

Falls es jemanden Interessiert: man kommt mit 7 Lemmata aus.

PS: Tipp: Offensichtliches sollte man auch immer beweisen :)

Benutzeravatar
Langbaeh
Mausschubser
Mausschubser
Beiträge: 56
Registriert: 16. Okt 2007 10:16
Wohnort: DA

Re: Praktikum 3

Beitrag von Langbaeh »

Ist es eigentlich gewollt, dass man ALLE Lemmata außer das "DP is complete" nur durch die eingebaute Generalize Funktion beweisen kann ? ^^

treo
Windoof-User
Windoof-User
Beiträge: 31
Registriert: 3. Okt 2007 21:58

Re: Praktikum 3

Beitrag von treo »

Wenn du erklären kannst was die einzelnen Lemmatas dann aussagen und warum sie hilfreicht sind, dann kannst du das sicher auch so machen, aber das solltest du dann wohl lieber beim Veranstalter nachfragen ;)

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

Re: Praktikum 3

Beitrag von aderhold »

Wie einige bereits bemerkt haben, ist die Lösung dieses Aufgabenblattes weniger umfangreich als die zur zweiten praktischen Übung. Insbesondere der Beweisaufwand ist geringer. Es sollte aber nicht vergessen werden, dass die Aufgabe nicht nur aus einer vf-Datei, sondern auch aus einer pdf-Datei besteht.

Um das Testat zu erhalten, reicht es nicht aus, nur eine "grüne Datei" einzureichen. Man muss auch mit dem Aufgabentext und dem vorgegebenen Algorithmus vertraut sein. Wie man das erreicht, bleibt jedem selbst überlassen. Wenn man die Beweisfehlschläge mit dem eigenen Kopf analysiert und selbst die Hilfslemmas formuliert, ist der Lerneffekt erfahrungsgemäß wesentlich größer als wenn man das andere (Kommilitonen oder seinen Rechner) erledigen lässt.

Kurz: Wer die Lösung selbst erarbeitet, ist dadurch schon gut für das Testatgespräch gerüstet; andernfalls muss man die zuerst eingesparte Arbeit später erbringen (natürlich noch vor dem Testatgespräch), um informiert zu sein.

Osterlaus
BSc Spammer
BSc Spammer
Beiträge: 1263
Registriert: 23. Aug 2007 12:46
Wohnort: DA

Re: Praktikum 3

Beitrag von Osterlaus »

Langbaeh hat geschrieben:Ist es eigentlich gewollt, dass man ALLE Lemmata außer das "DP is complete" nur durch die eingebaute Generalize Funktion beweisen kann ? ^^
Kann uns jemand einen Tipp geben, wie man das letzte Lemma, also DP is complete, am besten angeht? Bei allen anderen sind wir so naja vorangekommen, aber hier stockts nochmal richtig...

fl4$h g0rd0n
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 115
Registriert: 1. Okt 2007 22:20

Re: Praktikum 3

Beitrag von fl4$h g0rd0n »

1.) Was kann man Aussagen, wenn DavisPutnam(S) false zurückgibt?
2.) Was kann man mit dem Ergebnis von ComputeModel(S) machen?

Konkreteres darf ich wahrscheinlich nicht dazu sagen. Ich hoffe, es hilft dir trotzdem weiter.
"Education is the path from cocky ignorance to miserable uncertainty" -- Mark Twain

Osterlaus
BSc Spammer
BSc Spammer
Beiträge: 1263
Registriert: 23. Aug 2007 12:46
Wohnort: DA

Re: Praktikum 3

Beitrag von Osterlaus »

Ja, das hat schon weitergeholfen :) Wenn übrigens dieses Praktikum "leichter" als das mit den Binärbäumen gewesen sein soll, hoffe ich, dass das letzte nicht noch "leichter" wird ;)

Simon D
Windoof-User
Windoof-User
Beiträge: 24
Registriert: 17. Okt 2007 13:20

Re: Praktikum 3

Beitrag von Simon D »

hi
wir haben immer noch probleme mit dem
σ ⊫ S ∧ ∇⊧(σ, L) ∧ σ ⊧ ∼L → σ ⊫ split(L, S)
es irgendwie hängen wir da sehr fest.. kann gut sein das wir da über offensichtliches stopplern .. vlt. kann ja mal jemand en tipp geben..

Benutzeravatar
itportal2
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 236
Registriert: 25. Jan 2008 15:34
Wohnort: Darmstadt

Re: Praktikum 3

Beitrag von itportal2 »

Simon D hat geschrieben:hi
wir haben immer noch probleme mit dem
σ ⊫ S ∧ ∇⊧(σ, L) ∧ σ ⊧ ∼L → σ ⊫ split(L, S)
es irgendwie hängen wir da sehr fest.. kann gut sein das wir da über offensichtliches stopplern .. vlt. kann ja mal jemand en tipp geben..
Da kann man generalisieren. Versuch mal mit der eingabauten Funktion.

Simon D
Windoof-User
Windoof-User
Beiträge: 24
Registriert: 17. Okt 2007 13:20

Re: Praktikum 3

Beitrag von Simon D »

hab das gestern mal versucht .. beim 2. generalisieren hab ichs dann nach ne halben std abgebrochen...

Benutzeravatar
itportal2
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 236
Registriert: 25. Jan 2008 15:34
Wohnort: Darmstadt

Re: Praktikum 3

Beitrag von itportal2 »

Mach Prune bei dem Beweis von der Generalisation und dann generalisiere nochmal die Generalisation selbst. Sollte gehen.

Benutzeravatar
C0RNi666
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 114
Registriert: 8. Jan 2008 12:51

Re: Praktikum 3

Beitrag von C0RNi666 »

lol und wer lernt dabei, warum es funktioniert wie es funktioniert? :roll:
Win32: Reboot!
Unix: Be root!

Benutzeravatar
itportal2
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 236
Registriert: 25. Jan 2008 15:34
Wohnort: Darmstadt

Re: Praktikum 3

Beitrag von itportal2 »

Du kannst ja dann das Lemma sehen und evtl. verstehen. :wink:

Simon D
Windoof-User
Windoof-User
Beiträge: 24
Registriert: 17. Okt 2007 13:20

Re: Praktikum 3

Beitrag von Simon D »

C0RNi666 hat geschrieben:lol und wer lernt dabei, warum es funktioniert wie es funktioniert? :roll:
ja dann geb mir doch einen deiner meinung nach sinnvolleren tipp ... kriegen es ja so nich hin

Flipp
Neuling
Neuling
Beiträge: 10
Registriert: 20. Nov 2008 21:15

Re: Praktikum 3

Beitrag von Flipp »

Es gab hier im Forum mal eine Art Schema zum beweisen mit Verifun, das hat mir schon beim zweiten Praktikum sehr geholfen und auch beim dritten hat es funktioniert.

Im Prinzip braucht man dafür nichtmal wirkliches Verständniss des Stoffes, man muss einfach "von Hand generalisieren". Dazu lässt man den Beweis eines Lemmas automatisch ausführen, bis er irgendwann abbricht. Dann schneidet man den Beweisbaum am ersten Knoten mit "Move ..." ab und schaut sich den Beweis an dieser Stelle an. Die am weitesten eingerückten Terme müssen dann "von Hand" mit Lemmatas bewiesen werden. Oft sind diese alleine nicht gültig sondern nur unter den Bedingungen, unter denen sie in den eingerückten Ifs stehen. Das führt dann zu einem Lemma der Form " x < T => ?nothing(find(x, T))" (als Beispiel aus dem letzten Praktikum), diese vereinfachten Lemmata kann Verifun oft automatisch beweisen, ansonsten nochmal die gleiche Methode anwenden. Oft hilft es, einfach ganz allgemein sowas zu formulieren (eben einfach eine beliebige Zahl x und nicht hd(T2)), da aus der Allgemeingültigkeit auch folgt, dass es für das spezielle x = hd(T2) gilt, andersrum aber eben nicht. Ich hoffe ich habe das jetzt verständlich ausgedrückt, falls nicht schick mir ne PM mit der ICQ Nummer oso, bin denke ich den ganzen Tag noch hier ^^

Grüße
Flipp

Antworten

Zurück zu „Archiv“