HÜ 1.3: Refute wertet zu true aus

fetzer
Kernelcompilierer
Kernelcompilierer
Beiträge: 522
Registriert: 1. Okt 2008 17:18

HÜ 1.3: Refute wertet zu true aus

Beitrag von fetzer »

Hi,

wir haben die Lemmata aus Aufgabe 1.3 in Verifun ausprobiert und sind auf das Problem gestoßen, dass die Refute-Anweisung in Bezug auf eins unserer Beispiele beim "mix is injective"-Lemma zu true ausgewertet wird. Welche Aussage erhalten wir dadurch? IdR wird die Refute-Anweisung ja zu false ausgwertet. In den Folien habe ich dazu leider auch nichts gefunden.

Grüße

Benutzeravatar
AlexPi11
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 154
Registriert: 18. Apr 2009 15:32

Re: HÜ 1.3: Refute wertet zu true aus

Beitrag von AlexPi11 »

Naja - bewiesen ist bewiesen. Vll. hat Verifun ja gemerkt, dass das Lemma niemals unwahr wird.
Es geht ja auch anders herum, z.B: Simplification kann Lemma zu false auswerten.

Benutzeravatar
salted
Mausschubser
Mausschubser
Beiträge: 84
Registriert: 28. Sep 2009 21:21

Re: HÜ 1.3: Refute wertet zu true aus

Beitrag von salted »

fetzer hat geschrieben: Welche Aussage erhalten wir dadurch?
Das euer Beispiel nicht dazu geeignet ist, das Lemma zu widerlegen, weil die von euch gewählte Substitution eben das Lemma erfüllt.
AlexPi11 hat geschrieben:Naja - bewiesen ist bewiesen. Vll. hat Verifun ja gemerkt, dass das Lemma niemals unwahr wird.
Nein. Nur weil ein Lemma für einen einzelnen refute-Versuch (also für eine einzelne Substituion) zu true ausgewertet wird, heißt dies ja nicht, dass dies für alle möglichen Substituionen gilt (und nur in diesem Fall wäre das Lemma bewiesen).

Benutzeravatar
AlexPi11
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 154
Registriert: 18. Apr 2009 15:32

Re: HÜ 1.3: Refute wertet zu true aus

Beitrag von AlexPi11 »

Achso; ja - ich dachte das Lemma wurde zu true ausgewertet (grün); nicht nur der eine Refute-Versuch. Aber das war wohl nicht der Fall. ups

fetzer
Kernelcompilierer
Kernelcompilierer
Beiträge: 522
Registriert: 1. Okt 2008 17:18

Re: HÜ 1.3: Refute wertet zu true aus

Beitrag von fetzer »

salted hat geschrieben:
fetzer hat geschrieben: Welche Aussage erhalten wir dadurch?
Das euer Beispiel nicht dazu geeignet ist, das Lemma zu widerlegen, weil die von euch gewählte Substitution eben das Lemma erfüllt.
Ja, aber: Händisch eingesetzt resultiert unsere Belegung zum "false", welches im 2ten if-Statement steht. Ist durch eine Auswrtung zu einem false im Lemma denn eine Erfüllung dieses Lemmas?

Christoph Walther
Dozentin/Dozent
Beiträge: 86
Registriert: 1. Nov 2005 18:51

Re: HÜ 1.3: Refute wertet zu true aus

Beitrag von Christoph Walther »

fetzer hat geschrieben:wir haben die Lemmata aus Aufgabe 1.3 in Verifun ausprobiert und sind auf das Problem gestoßen, dass die Refute-Anweisung in Bezug auf eins unserer Beispiele beim "mix is injective"-Lemma zu true ausgewertet wird. Welche Aussage erhalten wir dadurch? IdR wird die Refute-Anweisung ja zu false ausgwertet. In den Folien habe ich dazu leider auch nichts gefunden.
Dann haben Sie nicht richtig hingeschaut. Die antwort auf Ihre frage steht auf folie 3/31. Am besten, Sie lesen sich abschnitt 3 von foliensatz 3 mal genau durch, dann sollte Ihnen der sachverhalt klar werden.

fetzer
Kernelcompilierer
Kernelcompilierer
Beiträge: 522
Registriert: 1. Okt 2008 17:18

Re: HÜ 1.3: Refute wertet zu true aus

Beitrag von fetzer »

Christoph Walther hat geschrieben: Dann haben Sie nicht richtig hingeschaut. Die antwort auf Ihre frage steht auf folie 3/31. Am besten, Sie lesen sich abschnitt 3 von foliensatz 3 mal genau durch, dann sollte Ihnen der sachverhalt klar werden.
Stimmt.
Dennoch die (nun konkrete) Frage: mix(1 :: ø, 2 :: 2 :: ø) = mix(1 :: 2 :: ø, 2 :: ø) wird zu true ausgewertet, somit muss der Term if{x1 = y1, x2 = y2, false} ausgewertet werden. Da offensichtlich x1 != y1 ist das Ergebnis des Lemmas "false" und damit wäre es doch widerlegt, oder nicht? Der "korrekte Vorgang" kommt auf das gleiche Ergebnis, also auch auf "false". Dennoch kommt es bei ersterem zu "true" und bei letzterem zu "false". Irgendwie finde ich den Denkfehler darin nicht...

Flipp
Neuling
Neuling
Beiträge: 10
Registriert: 20. Nov 2008 21:15

Re: HÜ 1.3: Refute wertet zu true aus

Beitrag von Flipp »

Wahrscheinlich habt ihr die Werte in der falschen Reihenfolge eingegeben (ist mir gerade beim Testen auch erstmal passiert):

Nach dem Klick auf "Refute" erwartet er die Substition in der Reihnfolge x1, y1, x2, y2, im Lemma heisst es dann "mix(x1, x2) = mix(y1, y2)". Wenn man nun also ohne nachzulesen ersetzt und die Variablen als "x1, x2, y1, y2" erwartet dann kommen eventuell unerwartete Ergebnisse heraus.

Grüße,
Philipp

Antworten

Zurück zu „Archiv“