Praktikum 3 - "DavisPutnam is complete"

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

Re: Praktikum 3 - "DavisPutnam is complete"

Beitrag 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.

philipp_m
Mausschubser
Mausschubser
Beiträge: 99
Registriert: 4. Dez 2010 18:10

Re: Praktikum 3 - "DavisPutnam is complete"

Beitrag 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?

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

Re: Praktikum 3 - "DavisPutnam is complete"

Beitrag 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.

philipp_m
Mausschubser
Mausschubser
Beiträge: 99
Registriert: 4. Dez 2010 18:10

Re: Praktikum 3 - "DavisPutnam is complete"

Beitrag 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?

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

Re: Praktikum 3 - "DavisPutnam is complete"

Beitrag von dschneid »

Ich würde an deiner Stelle mal hingehen...

philipp_m
Mausschubser
Mausschubser
Beiträge: 99
Registriert: 4. Dez 2010 18:10

Re: Praktikum 3 - "DavisPutnam is complete"

Beitrag von philipp_m »

dschneid hat geschrieben:Ich würde an deiner Stelle mal hingehen...
Hatte ich auch vor, wenn mir nichts anderes gesagt wird:)

SchottCh
Mausschubser
Mausschubser
Beiträge: 74
Registriert: 4. Okt 2010 16:39

Re: Praktikum 3 - "DavisPutnam is complete"

Beitrag von SchottCh »

Danke dschneid,
dein Tipp/Hilfe hat uns wirklich sehr geholfen.
Haben es dann auch sofort hinbekommen.
Vielen Dank!

Antworten

Zurück zu „Archiv“