Praktische Übung 4.1

Benutzeravatar
mba
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 260
Registriert: 13. Jul 2007 19:16

Praktische Übung 4.1

Beitrag von mba »

Hallo,
Beweisen Sie nun, dass die Prozedur DavisPutnam in der Datei Praxis4.vf terminiert.
Reicht es hier aus, wenn man die gleichen Lemmas benutzt, die auch in der Praktischen Übung 3 verwendet wurden? Mit den zwei Lemmas "DavisPutnam Termination 1 & 2" wird doch die Terminierung bewiesen oder verstehe ich etwas falsch?

Gruß

-m
»Es ist noch kein Meister vom Himmel gefallen«
Wenn doch, wär er jetzt tot.
Bild

Benutzeravatar
Maeher
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 282
Registriert: 14. Okt 2007 23:02
Kontaktdaten:

Re: Praktische Übung 4.1

Beitrag von Maeher »

Nein wird es nicht. Siehe Aufgabenstellung:
Die Terminierung des Verfahrens war in der vorgegebenen Datei axiomatisch festgelegt, d. h. sie wurde ohne Beweis als gegeben angenommen.
Sowas kann man in verifun mit bösen bösen Tricks :D anscheinend machen.

Du sollst jetzt einen richtigen Beweis machen.

Benutzeravatar
Langbaeh
Mausschubser
Mausschubser
Beiträge: 56
Registriert: 16. Okt 2007 10:16
Wohnort: DA

Re: Praktische Übung 4.1

Beitrag von Langbaeh »

Die Lemmas sind schon richtig im Prinzip, nur ist die measure Funktion aus dem dritten Praktikum nicht wirklich implementiert :)
Die müsstest du erstmal finden.

Benutzeravatar
mba
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 260
Registriert: 13. Jul 2007 19:16

Re: Praktische Übung 4.1

Beitrag von mba »

Hmmmm... also wäre measure(S : list[list[LITERAL]]) : ℕ eine Funktion, die die Anzahl der Elemente in list[list[LITERAL]] berechnet?
»Es ist noch kein Meister vom Himmel gefallen«
Wenn doch, wär er jetzt tot.
Bild

Christoph-D
Computerversteher
Computerversteher
Beiträge: 325
Registriert: 11. Dez 2005 13:14
Wohnort: Darmstadt

Re: Praktische Übung 4.1

Beitrag von Christoph-D »

mba hat geschrieben:Hmmmm... also wäre measure(S : list[list[LITERAL]]) : ℕ eine Funktion, die die Anzahl der Elemente in list[list[LITERAL]] berechnet?
Es ist genau Teil der Aufgabe, sich zu überlegen, ob so ein measure(x) für die Terminierung ausreicht. Um das zu beantworten, müsstest du wahrscheinlich erstmal "Anzahl der Elemente in list[list[LITERAL]]" genauer definieren.

Zum technischen: Es ist nicht unbedingt verlangt, einen einzigen Maßterm measure(x) zu finden. Man kann auch zwei Maßterme finden und diese dann in Verifun mit Komma getrennt eingeben, dann werden die lexikografisch kombiniert. Und ein Maßterm ist außerdem nicht auf direkte Funktionsaufrufe f(x) beschränkt. Falls es sinnvoll ist, kann man auch f(x) + g(x) als Maßterm nehmen oder irgendwas anderes.
"I believe in the fundamental interconnectedness of all things." (Dirk Gently)

Benutzeravatar
Gnomix
Computerversteher
Computerversteher
Beiträge: 306
Registriert: 31. Okt 2005 08:44

Re: Praktische Übung 4.1

Beitrag von Gnomix »

Christoph-D hat geschrieben:Zum technischen: Es ist nicht unbedingt verlangt, einen einzigen Maßterm measure(x) zu finden. Man kann auch zwei Maßterme finden und diese dann in Verifun mit Komma getrennt eingeben, dann werden die lexikografisch kombiniert. Und ein Maßterm ist außerdem nicht auf direkte Funktionsaufrufe f(x) beschränkt. Falls es sinnvoll ist, kann man auch f(x) + g(x) als Maßterm nehmen oder irgendwas anderes.
Ich stehe gerade vor dem Problem, dass ich eine verschachtelte measurefunktion erstellt habe.
Sprich Funktion A berechnet die Anzahl aller LITERALe in einer Klausel und Funktion B(measure) nutzt diese und sich selbst zum berechnen aller Literale in einer Klauselmenge.
Beide terminieren.

Versuche ich nun aber die beiden Terminierungslemmas aus Praktikum 3 zu verwenden mit meiner measure-Funktion bleibt der Beweis stehen.
Lemma:

Code: Alles auswählen

lemma DavisPutnam Termination 1 <= ∀ S : list[list[LITERAL]]
  if{?ø(S),
    true,
    if{?ø(hd(S)), true, length-C(S) > length-C(split(∼(hd(hd(S))), tl(S)))}}
Letztes Goal:

Code: Alles auswählen

if{?ø(hd(S)),
  true,
  if{?ø(tl(S)),
    true,
    length-S(hd(S)) + length-C(tl(S))
    > length-C(split(∼(hd(hd(S))), tl(S)))}}
Induction-Hypothese:

Code: Alles auswählen

IH-1:
if{?::(tl(S)),
  if{?ø(hd(tl(S))),
    true,
    if{?ø(tl(tl(S))),
      true,
      length-S(hd(tl(S))) + length-C(tl(tl(S)))
      > length-C(split(∼(hd(hd(tl(S)))), tl(tl(S))))}},
  true}
Ich komme einfach nicht weiter. :cry:

Hat jemand einen Tipp für mich ?

treo
Windoof-User
Windoof-User
Beiträge: 31
Registriert: 3. Okt 2007 21:58

Re: Praktische Übung 4.1

Beitrag von treo »

Prinzipiell musst du da auch gar nicht das verwenden was du aus Praktikum 3 hast, du hättest genau die gleichen Lemmas bekommen können nachdem du deinen Maßterm für die Terminierung angegeben hast. Rechts ist ein Feld wo die Terminierungshypotesen drinstehen und da kannst du sie auch rauskopieren.

Ansonsten was dein momentanes Problem angeht so solltest du in der Lage sein mit wenigen Lemmas das ganze zu beweisen, ich sehe da höchstens 2 notwendige drin, wobei eigentlich schon genau 2 für Davis Putnam reichen wenn man seine Maßterme geschickt wählt.

Antworten

Zurück zu „Archiv“