DavisPutnam is sound

mrzb6
Mausschubser
Mausschubser
Beiträge: 54
Registriert: 4. Okt 2010 21:50
Wohnort: Darmstadt

DavisPutnam is sound

Beitrag von mrzb6 »

Hey,

nach zahllosen Versuchen konnte ich noch keinen Fortschritt beim Beweis des Lemmas verzeichnen.
Es scheitert wohl daran, zu verstehen, was Verifun gerade fehlt (woran sonst?!).
Hat jemand schon ein bisschen grün in den Beweisbaum gebracht und kann einen Tipp geben, wie es funktionieren könnte? :mrgreen:

[-=thomas=-]
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 137
Registriert: 27. Apr 2009 10:47
Wohnort: Darmstadt

Re: DavisPutnam is sound

Beitrag von [-=thomas=-] »

Hi,

der Soundness-Beweis ist ja bereits in 5 Teilbäume aufgeteilt. Wenn Du im Proof Viewer des jeweiligen Teilbaumes "Highlight terms to prove goal" aktiviert hast, dann solltest Du versuchen, die jeweils grün markierten Ausdrücke - mit Hilfe (eines Teils) der Bedingungen zuvor - zu beweisen.

Beim ersten Teilbaum bspw. wäre das also eine dieser beiden Aussagen:
∇⊧(σ, hd(hd(S)))
σ ⊨ tl(hd(S)) \\ hd(hd(S))

Schreib Dir am besten auf ein Blatt Papier auf, was die einzelnen Funktionen bedeuten und jeweils zurück geben.

Ich hoffe das hilft etwas.

Gruß
Thomas
Tutor:
WS 11/12: FGdI 3, FoC
SS 11: CMS

Benutzeravatar
Domac
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 160
Registriert: 4. Okt 2010 16:11

Re: DavisPutnam is sound

Beitrag von Domac »

Um es vielleicht noch einmal klar hervorzuheben:
[-=thomas=-] hat geschrieben: Schreib Dir am besten auf ein Blatt Papier auf, was die einzelnen Funktionen bedeuten und jeweils zurück geben.
Ganz wichtig! Hat mir sehr geholfen.
Extend my dropbox space (here).
Thanks!

mrzb6
Mausschubser
Mausschubser
Beiträge: 54
Registriert: 4. Okt 2010 21:50
Wohnort: Darmstadt

Re: DavisPutnam is sound

Beitrag von mrzb6 »

[-=thomas=-] hat geschrieben: Schreib Dir am besten auf ein Blatt Papier auf, was die einzelnen Funktionen bedeuten und jeweils zurück geben.
Das habe ich bereits versucht (habe die Stelle, an der es hängt, zeilenweise in Worte gefasst), noch ohne Erfolg. Vielleicht krieg ichs ja irgendwie raus.

[-=thomas=-]
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 137
Registriert: 27. Apr 2009 10:47
Wohnort: Darmstadt

Re: DavisPutnam is sound

Beitrag von [-=thomas=-] »

Wenn Ihr an einer bestimmten Stelle hängt ist es sehr sinnvoll in die Poolsprechstunden zu gehen. Wir können Euch dann individuell Hilfestellungen geben und auf die richtige Fährte bringen.
Tutor:
WS 11/12: FGdI 3, FoC
SS 11: CMS

Benutzeravatar
DB_420
Mausschubser
Mausschubser
Beiträge: 89
Registriert: 24. Nov 2010 15:12

Re: DavisPutnam is sound

Beitrag von DB_420 »

mrzb6 hat geschrieben:
[-=thomas=-] hat geschrieben: Schreib Dir am besten auf ein Blatt Papier auf, was die einzelnen Funktionen bedeuten und jeweils zurück geben.
Das habe ich bereits versucht (habe die Stelle, an der es hängt, zeilenweise in Worte gefasst), noch ohne Erfolg. Vielleicht krieg ichs ja irgendwie raus.
In den einzelnen Schritten wird eine gegebene Belegung Sigma um Literale erweitert. Schaue dir mal genau an, welche Relevanz diese Literale für die Formel haben und formuliere Lemmata darüber.
Tutor:
Mathe II Inf (SS12)
Mathe I Inf (WS11/12)

nein23
Windoof-User
Windoof-User
Beiträge: 29
Registriert: 7. Okt 2009 18:15
Wohnort: Darmstadt

Re: DavisPutnam is sound

Beitrag von nein23 »

Hallo, trotz der bereits gegebenen Hilfe kommen wir immernoch nicht weiter. Uns ist einfach nicht klar, was genau wir beweisen oder zeigen müssen. Zwar ist klar was die Goals aussagen, aber nicht was man hier sinnvoll in Lemmata fassen kann oder soll.

Benutzeravatar
DB_420
Mausschubser
Mausschubser
Beiträge: 89
Registriert: 24. Nov 2010 15:12

Re: DavisPutnam is sound

Beitrag von DB_420 »

nein23 hat geschrieben:Hallo, trotz der bereits gegebenen Hilfe kommen wir immernoch nicht weiter. Uns ist einfach nicht klar, was genau wir beweisen oder zeigen müssen. Zwar ist klar was die Goals aussagen, aber nicht was man hier sinnvoll in Lemmata fassen kann oder soll.
Schau dir die DavisPutnam Prozedur nochmal genau an. Analog zu \rho gibt es ja hier 3 Fälle, die zu rekursiven Aufrufen führen. Die Fälle kannst du als Referenz nutzen.
Ich hoffe, das war jetzt nicht zu viel gesagt.
Tutor:
Mathe II Inf (SS12)
Mathe I Inf (WS11/12)

marcohyeah
Neuling
Neuling
Beiträge: 6
Registriert: 6. Jan 2012 18:24

Re: DavisPutnam is sound

Beitrag von marcohyeah »

DB_420 hat geschrieben: Schau dir die DavisPutnam Prozedur nochmal genau an. Analog zu \rho gibt es ja hier 3 Fälle, die zu rekursiven Aufrufen führen. Die Fälle kannst du als Referenz nutzen.
Ich hoffe, das war jetzt nicht zu viel gesagt.
DB_420 hat geschrieben: In den einzelnen Schritten wird eine gegebene Belegung Sigma um Literale erweitert. Schaue dir mal genau an, welche Relevanz diese Literale für die Formel haben und formuliere Lemmata darüber.
Danke erstmal für die Hilfestellung, allerdings hänge ich immernoch am Anfang der dritten Aufgabe. Ich scheine weder zu verstehen, was du mit "als Referenz nutzen" meinst (im gegebenen Zusammenhang), noch inwiefern Sigma um Literale erweitert wird. Mir fehlt einfach der Ansatzpunkt. Ich habe die 5 Goals nach der Fallunterscheidung soweit verstanden, und auch die Funktionen kenne ich sinngemäß fast auswendig, sooft bin ich sie durchgegangen. Trotzdem kann ich keinen sinnvollen Punkt finden an dem ich anfangen könnte zu arbeiten...

Benutzeravatar
Domac
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 160
Registriert: 4. Okt 2010 16:11

Re: DavisPutnam is sound

Beitrag von Domac »

@marcoyeah: dann besuche - wie schon erwähnt - die Pool-Sprechstunden. Wobei ich mir nicht vorstellen kann, dass das nicht zu lösen ist, wenn man schon alles auswendig kann. ;-) Vielleicht schaust du dir einfach nochmal an wie VeriFun arbeitet, dann kommst du vielleicht auf die Lösung. Vorallem ist es wichtig zu wissen, was das Programm machen soll und dann die gewünschte Semantik zu spezifizieren.

Gruß,
domac
Extend my dropbox space (here).
Thanks!

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: DavisPutnam is sound

Beitrag von dschneid »

Dafür ist es ein bisschen spät; die Abgabe ist ja schon am Sonntag und dann geht es gleich mit den Testaten los.

Vielleicht hier also einfach eine kleine Tele-Pool-Sprechstunde am Beispiel des ersten Teilbaumes von "DavisPutnam is sound":

Um zum Erfolg zu kommen, kann man einen der grün markierten Terme beweisen oder einen der rot markierten Terme widerlegen. Erst einmal schränkt man sich quasi den Suchraum ein: Manche Terme sind ganz offensichtlich kein guter Ansatzpunkt für einen Beweis, z.B. ist "?ø(hd(S))" sicher nicht immer wahr, "σ ⊫ tl(S)" nicht immer falsch, und so weiter. Diese Terme sind nur wichtig als zusätzliche Annahmen, unter denen man einen Term weiter "unten" in den verschachtelten if-Termen beweisen oder widerlegen will; es ist aber zwecklos, die Annahme selbst beweisen zu wollen. Über DavisPutnam selbst soll etwas gezeigt werden, also sollten die Hilfslemmata, die man formulieren wird, nicht wieder DavisPutnam enthalten; daher kann man auch die inneren beiden Terme vergessen. Letztlich bleiben zwei sinnvolle Terme übrig, die man zu beweisen oder widerlegen versuchen kann.

Man sollte bedenken, dass man beim Abstieg in einen if-Term die Gültigkeit bzw. Nicht-Gültigkeit der Bedingung annimmt, je nachdem, in welchen Zweig man absteigt. Man überlegt also bspw., ob "σ ⊨ tl(hd(S)) \\ hd(hd(S))" unter den Annahmen "?ø(hd(S))", "¬ σ ⊫ tl(S)", "¬ ∇⊧(σ, hd(hd(S)))", "σ ⊨ tl(hd(S))" und "σ ⊫ split(hd(hd(S)), tl(S))" gilt. Meistens kann man relativ schnell sehen, welche Annahmen tatsächlich relevant sind, indem man betrachtet, in welchen davon Teilterme auftauchen, die auch im untersuchten Term wieder vorkommen. Wenn es da wenige Gemeinsamkeiten gibt, macht eine Annahme offenbar keine Aussage über den Term. Beispiel: Die Annahme "¬ σ ⊫ tl(S)" ist für "σ ⊨ tl(hd(S)) \\ hd(hd(S))" wohl irrelevant, weil tl(S) darin gar nicht vorkommt; die Annahme "σ ⊨ tl(hd(S))" könnte dahingegen aber wichtig sein.

Mit diesen beiden Strategien, das Goal zielgerichteter anzuschauen, kommt man aus dem "Raten" heraus.

Dann muss man sich überlegen, was die einzelnen Aussagen bedeuten. Die Funktionen ⊨ und ⊫ sollten schon vom "Namen" her recht intuitiv sein, wenn man sich noch an FGdI 2 erinnert. Interessant ist noch, wann ∇⊧ für ein σ und ein L wahr ist; das lässt sich eigentlich sehr gut in Worte fassen, wenn man überlegt, dass ein σ eine aussagenlogische Interpretation darstellt und durch die enthaltenen Literale angegeben wird, ob eine Variable auf wahr oder falsch gesetzt ist. Schließlich sollte man sich vor Augen halten, dass es hier um Klauseln geht, also um Disjunktionen ("Veroderungen") von Variablen. Dann kann man z.B. darüber nachdenken, wie sich die Wahrheit einer Klausel bezüglich einer Interpretation verändert, wenn man Literale daraus streicht (was \\ ja gerade tut).

Wenn man jetzt überlegt hat, warum ein bestimmter Term unter bestimmten Annahmen gilt oder nicht, kann man das in ein Lemma gießen, indem man das Goal entsprechend generalisiert und die überflüssigen Hypothesen und Terme herausstreicht.

Benutzeravatar
DB_420
Mausschubser
Mausschubser
Beiträge: 89
Registriert: 24. Nov 2010 15:12

Re: DavisPutnam is sound

Beitrag von DB_420 »

dschneid hat geschrieben:..., wenn man überlegt, dass ein σ eine aussagenlogische Interpretation darstellt und durch die enthaltenen Literale angegeben wird, ob eine Variable auf wahr oder falsch gesetzt ist...
Wobei das ganz interessant hier ist: Ich konnte ein Lemma beweisen, das aussagt, dass L und ~L nicht beide in einer Interpretation enthalten sein können; aber auch eines, das sagt, wenn L in einer Klausel enthalten ist, jede beliebige Interpretation L :: σ die Klausel erfüllt. Also insbesondere auch alle \sigma, welche ~L enthalten. Sprich: σ muss hier offenbar keine Funktion sein.
Tutor:
Mathe II Inf (SS12)
Mathe I Inf (WS11/12)

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

Re: DavisPutnam is sound

Beitrag von Christoph Walther »

marcohyeah hat geschrieben: Danke erstmal für die Hilfestellung, allerdings hänge ich immernoch am Anfang der dritten Aufgabe. Ich scheine weder zu verstehen, was du mit "als Referenz nutzen" meinst (im gegebenen Zusammenhang), noch inwiefern Sigma um Literale erweitert wird. Mir fehlt einfach der Ansatzpunkt. Ich habe die 5 Goals nach der Fallunterscheidung soweit verstanden, und auch die Funktionen kenne ich sinngemäß fast auswendig, sooft bin ich sie durchgegangen. Trotzdem kann ich keinen sinnvollen Punkt finden an dem ich anfangen könnte zu arbeiten...
Dann versuchen Sie das problem erst mal mit papier und bleistift zu lösen, oder zumindest den lösungsweg zu skizzieren. Also: Was bedeutet "DP is sound"? Welche begriffe benötige ich um diese behauptung zu formulieren (vielleicht mal zur erinnerung im FGdI 2 skript nachschauen). Wenn das klar ist, dann geht es an den beweis. Der wird durch induktion geführt, das sieht man ja schon in der vf-datei der aufgabe. Das kann man ja als ansatz für die manuelle lösung verwenden. Vielleicht bemerken Sie dabei, daß sie grundlegenede schwierigkeiten haben, die aufgabenstellung überhaupt zu verstehen. Dann müssen Sie erstmal dieses problem (=> stoff von FGdI 2) lösen. Sobald Sie verstanden haben, was man beweisen muß & wie das geht, so können Sie die lösung auch mit VeriFun erstellen. Das ist wie mit einem texteditor, mit dem man einen aufsatz zu irgendeinem thema schreiben will. Hat man keine idee, was man schreiben soll, so hilft der editor auch nicht.

marcohyeah
Neuling
Neuling
Beiträge: 6
Registriert: 6. Jan 2012 18:24

Re: DavisPutnam is sound

Beitrag von marcohyeah »

Danke nochmal an alle, der Aufgabenteil ist geschafft!

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: DavisPutnam is sound

Beitrag von dschneid »

DB_420 hat geschrieben:Wobei das ganz interessant hier ist: Ich konnte ein Lemma beweisen, das aussagt, dass L und ~L nicht beide in einer Interpretation enthalten sein können; aber auch eines, das sagt, wenn L in einer Klausel enthalten ist, jede beliebige Interpretation L :: σ die Klausel erfüllt. Also insbesondere auch alle \sigma, welche ~L enthalten. Sprich: σ muss hier offenbar keine Funktion sein.
Das ist tatsächlich ganz interessant: Durch die Art, wie die Modellbeziehungen implementiert sind, wird implizit festgelegt, wie das Auftauchen von sowohl positiven als auch negierten Literalen derselben Variable in einer Interpretation ausgelegt werden soll. Da beim ersten Auftreten eines Literals abgebrochen wird, ist nur dieses erste Literal relevant. Dein zweites Lemma konntest du beweisen, weil in L :: σ die positive Festlegung von L vor jedem eventuellen ~(L) steht.

Mir ist nicht ganz klar, was genau du damit meinst, dass L und ~L nicht beide in einer Interpretation enthalten sein können. Solche Listen von Literalen kann man sicherlich aufschreiben, davon hält einen nichts ab; du meinst wohl etwas anderes.

Antworten

Zurück zu „Archiv“