Praktikum 3 - "DavisPutnam is complete"

[DB_420]

Hallo,

hat jemand einen Hinweis für den 1. Induktionsschritt bei o.g. Lemma? Den 2. Schritt haben wir bereits bewiesen (2 Lemmata), die Fallunterscheidung beim 1. Schritt haben wir mit den DavisPutnam(...)-Termen versucht, kommen aber jetzt nicht weiter. Es fehlt anscheinend ein Lemma, das DavisPutnam und Rho irgendwie in Verbindung setzt.

[dschneid]

Ganz im Gegenteil; sowohl DavisPutnam als auch \(\rho\) müssen eigentlich immer herausgeneralisiert werden.

[DB_420]

Ganz im Gegenteil; sowohl DavisPutnam als auch \(\rho\) müssen eigentlich immer herausgeneralisiert werden.

Hat zwar noch ganz schön gedauert, aber danke für den Hinweis, so haben wir wenigstens nicht in der falschen Richtung gesucht.
Interessanterweise waren alle Lemmata bis auf eines schon vorhanden, nur Verifun hat sie nicht angewendet. Erst beim X. ten Versuch und einem Klick
auf "Purge" ging es...

[Christoph Walther]

Interessanterweise waren alle Lemmata bis auf eines schon vorhanden, nur Verifun hat sie nicht angewendet. Erst beim X. ten Versuch und einem Klick
auf "Purge" ging es...

Wenn ein lemma fehlt, kann das schon entscheidend sein für die automatische anwendung aller erforderlichen lemmata sein. In unserer lösung werden alle lemmata automatisch angewendet. Aber hier noch ein tip: In der mathematik versucht man immer die schwächsten voraussetzungen für ein lemma zu formulieren. Wenn man jetzt ein lemma "entwirft", etwa mittels generalisierung, so kann es passieren, daß dort nicht benötigte voraussetzungen "übrig bleiben". Das lemma wird bewiesen und später wundert man sich, daß es nicht angewendet wird. Grund ist dann, daß die überflüssige voraussetzung eben auch erfüllt sein muß. Kurzum: Je weniger voraussetzungen man formuliert, desto anwendbarer ist ein lemma.

[DB_420]

Es ist doch ziemlich bemerkenswert, was diese Voraussetzungen machen, danke für den Tip. Bei einem Lemma (es verwendet als Variable die Liste S) habe ich die Voraussetzung ?::(S) mal entfernt, und plötzlich konnte das System das Lemma ohne Hilfe beweisen. Mit der Voraussetzung gab's anscheinend keinen vernünftigen Induktionsanfang... jedenfalls erstaunlich, was das System kann!
Vielen Dank auf jedenfall für den Tip!

[Christoph Walther]

Es ist doch ziemlich bemerkenswert, was diese Voraussetzungen machen, danke für den Tip. Bei einem Lemma (es verwendet als Variable die Liste S) habe ich die Voraussetzung ?::(S) mal entfernt, und plötzlich konnte das System das Lemma ohne Hilfe beweisen. Mit der Voraussetzung gab's anscheinend keinen vernünftigen Induktionsanfang...

Das ist ein anderer effekt. Ich meinte, daß die anwendwendbarkeit von lemmata mit überflüssigen voraussetzungen gemindert wird. Sie meinen, daß auch die beweise schwieriger werden. Da haben Sie recht & dies ist ein weiterer grund, sich genau anzuschauen, ob voraussetzungen wirklich erforderlich sind. Hier ein einfaches experiment:

function [infixr,20] +(x : ℕ, y : ℕ) : ℕ <= if ?0(x) then y else ⁺(⁻(x) + y) end_if

lemma + is associative <= ∀ x, y, z : ℕ(x + y) + z = x + y + z

Wird mit Verify allein durch symbolische auswertung bewiesen.

Jetzt Modify zu: lemma + is associative <= ∀ z, x, y : ℕif{¬ ?0(x), (x + y) + z = x + y + z, true}

Auch hier ist Verify erfolgreich, benötigt aber ein Use Lemma um die induktionshypothese anzuwenden.

Jetzt Modify zu: lemma plus_associative <= ∀ z, x, y : ℕif{x > y, (x + y) + z = x + y + z, true}

Verify scheitert. Da das beweisziel mit der (überflüssigen) vorraussetzung schwächer ist, ist auch die induktionshypothese schwächer. In diesem fall nicht anwendbar, also scheitert der beweis. Hat nichts mit VeriFun zu tun sondern nur mit Mathematik - auch ein manueller beweis ist umständlich (wenn überhaupt möglich).

[SchottCh]

Hallo,
wir haben den 2 Schritt auch schon bewiesen und auch schon generell ziemlich viele Lemma geschrieben. Hat vielleicht jemand einen Tipp für uns zum vorgehen ? Danke schon mal.

[radix89]

Hallo,
wir haben den 2 Schritt auch schon bewiesen und auch schon generell ziemlich viele Lemma geschrieben. Hat vielleicht jemand einen Tipp für uns zum vorgehen ? Danke schon mal.

Ist bei uns dasselbe...

[nein23]

Schließe mich der Gruppe der Ratlosen an

Ein Hinweis oder Denkanstoss zur caseanalysis wäre sicher sehr hilfreich. Uns ist u.a. nicht klar wie man darauf kommt welche Fälle relevant sind und wie man hier sinnvoll vorgeht bzw cases "findet". Orientiert man sich am Goal oder an den Funktionen Rho bzw. DavisPutnam?

[dschneid]

Mit der Case Analysis will man nur das eher große Goal in zwei kleinere, einfacher zu behandlende aufteilen. Man nimmt also als Case Term einfach die äußerste Bedingung des Goals.

Der Beweis funktioniert genauso gut ohne die Case Analysis; das soll es nur einfacher machen, die Sache zu überblicken.

[schmusedrache]

Hilfe!!
wo sollen wir bei das davisputnam weg generaliesiern?
soll man das schon bei der case analyse machen? und sollte man die nach der case analyse neuen cases wieder mti case analysen aufteilen?

danke für eure hilfe

[Senchy]

Falls jemand noch einen Tipp zu dem Lemma hat sind wir sicherlich nicht die einzigen die sich darüber freuen würden...
Uns fehlt von dem Lemma nur noch der obere Ast, und bei beiden Fällen kommen wir seit 2 Tagen nicht wirklich weiter.
Die Fallunterscheidung macht es zwar lesbarer, aber ein Ansatz was man in etwas aus dem Goal ziehen soll wäre echt super.
Gruß

[philipp_m]

Ich wäre auch für sämtliche Tipps dankbar... wenn ich nämlich DavisPutnam und p herausgeneralisiere, bleibt bei mir in beiden Subtrees nichts mehr brauchbares über. Wie sieht denn bei euch der Beweisbaum ohne zusätzliche Lemmata aus?
Bei mir:
Induktion mit 3 Subtrees:
1. Subtree automatisch bewiesen
2. Subtree: 6 Schritte, dann neue Induktion mit 1. Teil automatisch bewiesen, 2. Teil hängt nach 2 Schritten (Hier Case Analysis?)
3. Subtree: 3 Schritte, dann neue Induktion mit 1. Teil automatisch bewiesen, 2. Teil hängt nach 2 Schritten

[marcohyeah]

Der 3te Subtree ist bei uns grün(mit den nötigen Lemmas versteht sich). Ansonsten machen wir an der von dir genannten Stelle die Fallunterscheidung, kommen da aber auch nicht weiter...

[dschneid]

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.