Praktikum 3 - "DavisPutnam is complete"
Praktikum 3 - "DavisPutnam is complete"
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.
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.
Tutor:
Mathe II Inf (SS12)
Mathe I Inf (WS11/12)
Mathe II Inf (SS12)
Mathe I Inf (WS11/12)
Re: Praktikum 3 - "DavisPutnam is complete"
Ganz im Gegenteil; sowohl DavisPutnam als auch \(\rho\) müssen eigentlich immer herausgeneralisiert werden.
Re: Praktikum 3 - "DavisPutnam is complete"
Hat zwar noch ganz schön gedauert, aber danke für den Hinweis, so haben wir wenigstens nicht in der falschen Richtung gesucht.dschneid hat geschrieben:Ganz im Gegenteil; sowohl DavisPutnam als auch \(\rho\) müssen eigentlich immer herausgeneralisiert werden.
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...
Tutor:
Mathe II Inf (SS12)
Mathe I Inf (WS11/12)
Mathe II Inf (SS12)
Mathe I Inf (WS11/12)
-
- Dozentin/Dozent
- Beiträge: 86
- Registriert: 1. Nov 2005 18:51
Re: Praktikum 3 - "DavisPutnam is complete"
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 hat geschrieben:dschneid hat geschrieben: 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...
Re: Praktikum 3 - "DavisPutnam is complete"
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!
Vielen Dank auf jedenfall für den Tip!
Tutor:
Mathe II Inf (SS12)
Mathe I Inf (WS11/12)
Mathe II Inf (SS12)
Mathe I Inf (WS11/12)
-
- Dozentin/Dozent
- Beiträge: 86
- Registriert: 1. Nov 2005 18:51
Re: Praktikum 3 - "DavisPutnam is complete"
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:DB_420 hat geschrieben: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...
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).
Re: Praktikum 3 - "DavisPutnam is complete"
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.
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.
Re: Praktikum 3 - "DavisPutnam is complete"
Ist bei uns dasselbe...SchottCh hat geschrieben: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.
Re: Praktikum 3 - "DavisPutnam is complete"
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?

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?
Re: Praktikum 3 - "DavisPutnam is complete"
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.
Der Beweis funktioniert genauso gut ohne die Case Analysis; das soll es nur einfacher machen, die Sache zu überblicken.
-
- Neuling
- Beiträge: 1
- Registriert: 6. Jan 2012 17:57
Re: Praktikum 3 - "DavisPutnam is complete"
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
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
Re: Praktikum 3 - "DavisPutnam is complete"
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ß
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ß
Re: Praktikum 3 - "DavisPutnam is complete"
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
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
-
- Neuling
- Beiträge: 6
- Registriert: 6. Jan 2012 18:24
Re: Praktikum 3 - "DavisPutnam is complete"
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...
Re: Praktikum 3 - "DavisPutnam is complete"
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:
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:
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.
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}}}
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))}
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.