Seite 2 von 2

Re: Praktikum 3 - "DavisPutnam is complete"

Verfasst: 8. Jan 2012 20:08
von nein23
oh man....versucht mal die case analysis weiter am anfang des beweisbaums zu machen...
wir haben immer versucht am ende des baums zu arbeiten was uns nichts gebraucht hatte. als wir dann mal weiter oben abgeschnitten haben konnten wir sofort alles beweisen.

Re: Praktikum 3 - "DavisPutnam is complete"

Verfasst: 8. Jan 2012 21:24
von philipp_m
dschneid hat geschrieben:Das Problem ist hier, dass nicht alle Annahmen, die man in einem Lemma verwenden könnte, im Goal-Term stehen. Weitere Annahmen folgen aber aus der Induktionshypothese.

Nehmen wir als Beispiel den ersten Fall; das Goal ist:

Code: Alles auswählen

if{?ø(hd(S)),
  true,
  if{DavisPutnam(split(∼(hd(hd(S))), tl(S))),
    true,
    if{DavisPutnam((tl(hd(S)) \\ hd(hd(S))) :: split(hd(hd(S)), tl(S))),
      hd(hd(S)) :: ρ(split(∼(hd(hd(S))), tl(S))) ⊫ tl(S),
      true}}}
Wenn man bedenkt, dass man mit den DavisPutnam-Termen nichts anfangen kann, bleibt da überhaupt keine Annahme übrig, um den innersten Term zu beweisen. Nun lautet aber die erste Induktionshypothese:

Code: Alles auswählen

if{DavisPutnam(split(∼(hd(hd(S))), tl(S))),
  true,
  ρ(split(∼(hd(hd(S))), tl(S))) ⊫ split(∼(hd(hd(S))), tl(S))}
Das heißt, wenn DavisPutnam(split(∼(hd(hd(S))), tl(S))) nicht gilt, dann gilt ρ(split(∼(hd(hd(S))), tl(S))) ⊫ split(∼(hd(hd(S))), tl(S)). Für den Term, den wir zeigen wollen, gilt DavisPutnam(split(∼(hd(hd(S))), tl(S))) nicht, also können wir ρ(split(∼(hd(hd(S))), tl(S))) ⊫ split(∼(hd(hd(S))), tl(S)) hier annehmen.

Wenn man die zusätzlichen Annahmen alle in den Goal-Term haben will, kann man die Induktionshypothese mit Use Lemma manuell auf den innersten Term anwenden. VeriFun wird das dann alles wieder rausrechnen, deswegen muss man die folgende Simplification abschneiden. Um den Term dennoch etwas leichter verstehen zu können, kann man stattdessen eine Weak Normalization machen.

Dann kann man überlegen, wieso die Annahme ρ(split(∼(hd(hd(S))), tl(S))) ⊫ split(∼(hd(hd(S))), tl(S)) den Term hd(hd(S)) :: ρ(split(∼(hd(hd(S))), tl(S))) ⊫ tl(S) impliziert, und entsprechend generalisieren.
Also bei mir existiert das von dir genannte Goal im kompletten Beweisbaum nicht, meine letzten Goalterme lauten:

Code: Alles auswählen

if{?ø(hd(S)),
  true,
  if{∼(hd(hd(S))) ∈∈ tl(S),
    if{DavisPutnam((tl(hd(S)) \\ hd(hd(S))) :: split(hd(hd(S)), tl(S))),
      if{DavisPutnam(split(∼(hd(hd(S))), tl(S))),
        true,
        hd(hd(S)) :: ρ(split(∼(hd(hd(S))), tl(S))) ⊫ tl(S)},
      if{
       ∼(hd(hd(S)))
       :: ρ((tl(hd(S)) \\ hd(hd(S))) :: split(hd(hd(S)), tl(S)))
       ⊨ hd(S),
       if{?::(tl(S)),
         if{?ø(hd(tl(S))),
           false,
           if{∼(hd(hd(tl(S)))) ∈∈ tl(tl(S)),
             if{DavisPutnam(split(∼(hd(hd(tl(S)))), tl(tl(S)))),
               if{
                DavisPutnam(
                 (tl(hd(tl(S))) \\ hd(hd(tl(S)))) :: split(hd(hd(tl(S))), tl(tl(S)))),
                false,
                ∼(hd(hd(S)))
                :: ρ((tl(hd(S)) \\ hd(hd(S))) :: split(hd(hd(S)), tl(S)))
                ⊫ tl(S)},
               ∼(hd(hd(S)))
               :: ρ((tl(hd(S)) \\ hd(hd(S))) :: split(hd(hd(S)), tl(S)))
               ⊫ tl(S)},
             ∼(hd(hd(S)))
             :: ρ((tl(hd(S)) \\ hd(hd(S))) :: split(hd(hd(S)), tl(S)))
             ⊫ tl(S)}},
         true},
       false}},
    true}}
und

Code: Alles auswählen

if{?ø(hd(S)),
  true,
  if{?::(tl(S)),
    if{DavisPutnam(tl(S)),
      true,
      if{ρ(tl(S)) ⊫ tl(S),
        if{∼(hd(hd(S))) ∈∈ tl(S), true, hd(hd(S)) :: ρ(tl(S)) ⊫ tl(S)},
        true}},
    true}}
Kann es sein, dass hier normalerweise irgendwo ein Lemma aus der 3.2 angewendet werden sollte, das bei mir nicht angewandt wird?

Re: Praktikum 3 - "DavisPutnam is complete"

Verfasst: 8. Jan 2012 23:38
von dschneid
Wir reden von zwei verschiedenen Dingen: Ich meine die beiden Fälle, die man nach der Case Analysis im ersten Zweig erhät; du aber meinst die beiden Zweige in den verschiedenen Induktionsschritten. Du wirst vielleicht sehen, dass mein Goal ein Teil des ersten Terms ist, den du gepostet hast.

Re: Praktikum 3 - "DavisPutnam is complete"

Verfasst: 9. Jan 2012 00:02
von philipp_m
dschneid hat geschrieben:Wir reden von zwei verschiedenen Dingen: Ich meine die beiden Fälle, die man nach der Case Analysis im ersten Zweig erhät; du aber meinst die beiden Zweige in den verschiedenen Induktionsschritten. Du wirst vielleicht sehen, dass mein Goal ein Teil des ersten Terms ist, den du gepostet hast.
Ja, ist mir in der Zwischenzeit auch aufgefallen, auch wenn ich mit keiner Case Analysis genau auf den von dir geposteten Teil gekommen bin.
Habe inzwischen meine unvollständige Aufgabe hochgeladen, aber ich gehe mal nicht davon aus, dass es so überhaupt Sinn macht, zum Testat zu erscheinen, wenn die letzte Aufgabe nicht durchläuft, oder?

Re: Praktikum 3 - "DavisPutnam is complete"

Verfasst: 9. Jan 2012 00:06
von dschneid
Ich würde an deiner Stelle mal hingehen...

Re: Praktikum 3 - "DavisPutnam is complete"

Verfasst: 9. Jan 2012 00:28
von philipp_m
dschneid hat geschrieben:Ich würde an deiner Stelle mal hingehen...
Hatte ich auch vor, wenn mir nichts anderes gesagt wird:)

Re: Praktikum 3 - "DavisPutnam is complete"

Verfasst: 9. Jan 2012 10:32
von SchottCh
Danke dschneid,
dein Tipp/Hilfe hat uns wirklich sehr geholfen.
Haben es dann auch sofort hinbekommen.
Vielen Dank!