?mkbyte(x)

Benutzeravatar
Anne
Mausschubser
Mausschubser
Beiträge: 74
Registriert: 2. Jan 2007 20:39

?mkbyte(x)

Beitrag von Anne »

Was genau bedeutet "?mkbyte(x)" (als von Verifun erzeugte Hypothese)?

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Beitrag von yourmaninamsterdam »

Der Ausdruck fragt grundsätzlich nach dem Typ von x.
Also ?mkbyte(x) ist sowas wie (x instanceof mkbyte). Ähnliche Aussagen sind ?0(x)... die bedeuten sowas wie (x == 0).

Die Hypothese sagt dir, dass Verifun anschließend annimmt, diese Behauptung sei wahr. Das ist vor allem dann gegeben, wenn es sich in der else-Klausel um etwas handelt, das true ist.
Wenn da also
if{?mkbyte(x), Ausdruck, true}
steht, wird Verifun anschließend annehmen, ?mkbyte(x) sei true. Es ist dann also nur noch "Ausdruck" zu beweisen.

Benutzeravatar
Anne
Mausschubser
Mausschubser
Beiträge: 74
Registriert: 2. Jan 2007 20:39

Beitrag von Anne »

Danke :-)

aderhold
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 212
Registriert: 21. Okt 2005 10:50

Re:

Beitrag von aderhold »

yourmaninamsterdam hat geschrieben:Wenn da also
if{?mkbyte(x), Ausdruck, true}
steht, [...]
... kann man entweder versuchen zu zeigen, dass x nicht von der Form mkbyte(...) ist (denn dann wertet der If-Ausdruck zu true aus) oder man zeigt, dass Ausdruck gilt und darf dabei verwenden, dass x von der Form mkbyte(...) ist.

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

Re: ?mkbyte(x)

Beitrag von Christoph Walther »

Anne hat geschrieben:Was genau bedeutet "?mkbyte(x)" (als von Verifun erzeugte Hypothese)?
Siehe formeln (3.1) und (3.2) auf seite 17 in http://www.inferenzsysteme.informatik.t ... -06-01.pdf .

Notschko
Windoof-User
Windoof-User
Beiträge: 40
Registriert: 27. Nov 2005 18:00
Wohnort: Frankfurt
Kontaktdaten:

Re: ?mkbyte(x)

Beitrag von Notschko »

Heisst das, um diese Hypothese beweisen zu können muss ein eigenes Lemma angelegt werden, welches diesen Fall abdeckt?

Sind eigen erstellte Lemmas für die 3.1. b) gültig? Oder dürfen nur die bereits vorhandenen Lemmas verwendet werden?

Dankeschööön!

Benutzeravatar
Maradatscha
Computerversteher
Computerversteher
Beiträge: 353
Registriert: 2. Okt 2006 18:53

Re: ?mkbyte(x)

Beitrag von Maradatscha »

beweisen geht nur durch Lemmata, wenn Verifun es nicht direkt ohne zwischenschritte automatisch macht.
Die Aufgabe ist gerade die richtigen Lemmata zu finden!

Benutzeravatar
MisterD123
Geek
Geek
Beiträge: 811
Registriert: 31. Okt 2006 20:04
Wohnort: Weiterstadt

Re: ?mkbyte(x)

Beitrag von MisterD123 »

teilweise hilft es auch, dem verifer von hand zu sagen, wie er welches lemma anwenden soll, hat bei uns einen grünen mehr gebracht ^^ allerdings verzeifeln wir grade an der d und f der zweiten aufgabe, das wfbyte funktioniert aber irgendwie kriegen wir die beweise nich hin x)

yourmaninamsterdam
Nerd
Nerd
Beiträge: 681
Registriert: 26. Okt 2006 14:04
Kontaktdaten:

Re: ?mkbyte(x)

Beitrag von yourmaninamsterdam »

Achtet mal darauf, wie ihr eure 0 darstellt.

Antworten

Zurück zu „Archiv“