Die Suche ergab 86 Treffer

von Christoph Walther
24. Mär 2009 00:18
Forum: Archiv
Thema: Fehler in Kapitel 6?: > der Relationsbeschreibungen
Antworten: 2
Zugriffe: 307

Re: Fehler in Kapitel 6?: > der Relationsbeschreibungen

fl4$h g0rd0n hat geschrieben:Meiner Meinung nach müsste die zweite Bedingung wie folgt lauten: \(\exists \delta\in\Delta.\forall i\in\{1 \dots k\}.\hspace{2pt} eval_P(\theta (\delta (x_i)) = r_i\)
Tatsächlich ein Fehler im Skript. Korrekterweise muß es so lauten wie in dem zitierten Korrekturvorschlag.
von Christoph Walther
30. Jan 2009 20:50
Forum: Archiv
Thema: Auswertung von Termen
Antworten: 2
Zugriffe: 351

Re: Auswertung von Termen

Es gibt noch einen weiteren grund: Die symbolische auswertung muß ja die "richtige" auswertung durch den interpreter "eval_P" reflektieren. Formal heißt das: Wenn t symbolisch zu r ausgewertet wird, so werden jede konstruktorgrundinstanz t' und die entsprechende konstruktorgrundinstanz r' von r durc...
von Christoph Walther
4. Dez 2008 23:01
Forum: Archiv
Thema: Hausaufgabe 2.2
Antworten: 2
Zugriffe: 204

Re: Hausaufgabe 2.2

... die Herleitungsregeln sagen nirgendwo explizit, dass bei if\{a, b, c\} eval_p(a) boolean sein soll. Da die Sprache des kalküls grundterme sind, muß man davon ausgehen, daß diese syntaktisch korrekt sind. Also gilt insbesondere, daß die typen der argumente einer funktionsanwendung instanzen der ...
von Christoph Walther
1. Dez 2008 21:21
Forum: Archiv
Thema: Reduzierte Anforderung bei "Praktische Übung 2"
Antworten: 7
Zugriffe: 758

Re: Reduzierte Anforderung bei "Praktische Übung 2"

Fl4sh hat geschrieben:Ich habe nur Angst, dass so eine "Fehleinschätzung" dann auch in der Klausur passiert. :(
Sowas kann man auch bei aller sorgfalt nie ausschließen, aber bei der bewertung der klausuren würde das dann schon berücksichtigt.

cw.
von Christoph Walther
29. Nov 2008 22:30
Forum: Archiv
Thema: Reduzierte Anforderung bei "Praktische Übung 2"
Antworten: 7
Zugriffe: 758

Re: Reduzierte Anforderung bei "Praktische Übung 2"

Wirklich toll wäre es, wenn bei der nächsten Aufgabe von vorne herein bedacht würde, dass wir Studenten den Umgang mit VF erst lernen und noch nicht jahrelange Erfahrung damit haben und deswegen auch für erfahrene Nutzer trivial aussehende Schritte sehr lange dauern können. Das versuchen wir schon ...
von Christoph Walther
25. Nov 2008 20:01
Forum: Archiv
Thema: Vorlesungsersatztermin für den 16.12.2008 am 12.12.2008
Antworten: 0
Zugriffe: 163

Vorlesungsersatztermin für den 16.12.2008 am 12.12.2008

Am 16.12.2008 fällt die Vorlesung wegen Belegung des Hörsaals C205 durch die TUD-Verwaltung aus. Stattdessen findet eine Vorlesung am Freitag, den 12.12.2008 von 11:40 bis 13:20 in S2|02/C205 statt.

cw.
von Christoph Walther
20. Nov 2008 22:27
Forum: Archiv
Thema: Trick für Lemma-Ideen ?
Antworten: 2
Zugriffe: 283

Re: Trick für Lemma-Ideen ?

Lange Rede, kurzer Sinn - meine Frage wäre: Gibt's da eventuell irgendwelche Tricks, mit denen man rausfinden / sehen kann, welches Lemma man jetzt braucht? Weil schwer waren die beiden in dem Fall ja nicht, aber ich komme nicht drauf, dass so etwas wie ""x != +(x + y)" gebraucht werden könnte. Vie...
von Christoph Walther
18. Nov 2008 19:42
Forum: Archiv
Thema: Frage Hausuebung 1 bei Aufgabe 1.b
Antworten: 4
Zugriffe: 270

Re: Frage Hausuebung 1 bei Aufgabe 1.b

Warum ignoriert das Verifun Programm wenn ich folgendes versuche, also die Fkt ggT hat dann die Farbe grau. Jedes programmelement besitzt einen zustand. Die zustände werden durch die farben angezeigt. Farbe "grau" eines prozeduricons bedeutet, daß die prozedur im zustand "ignored" ist (s. 'Legend' ...
von Christoph Walther
20. Aug 2008 14:57
Forum: Jobs
Thema: Mathe-Nachhilfe f. Realschule 9. Klasse gesucht
Antworten: 0
Zugriffe: 676

Mathe-Nachhilfe f. Realschule 9. Klasse gesucht

von privat für 90 min/woche. Bei interesse bitte e-mail an Chr.Walther@informatik.tu-darmstadt.de.

cw.
von Christoph Walther
20. Jan 2008 15:35
Forum: Archiv
Thema: Praktische Übung 4: qsort sorts lemma
Antworten: 10
Zugriffe: 1310

Re: Praktische Übung 4: qsort sorts lemma

Ein lemma ist falsch, wenn das lemma den zustand 'falsified' erhält. Dies erkannt man an der rot-färbung des lemma-icons im Program Viewer. Falls dies bei Ihnen der fall ist, so haben sie mindestens eine der hilfsprozeduren falsch implementiert. Der Disprover ersetzt alle allquantifizierten variable...
von Christoph Walther
9. Jan 2008 19:28
Forum: Archiv
Thema: Klausurrelevante Themen
Antworten: 7
Zugriffe: 1410

Klausurrelevante Themen

Heute war die fachschaft bei mir, um über die vorlesung zu sprechen. Dabei hat sich auch herausgestellt, daß für den ersten teil der vorlesung nicht der von mir verwendete (gekürzte) foliensatz auf der webseite steht, sondern der originalfoliensatz - mein fehler. Man hat mir gesagt, daß dies zu irri...
von Christoph Walther
8. Jan 2008 19:20
Forum: Archiv
Thema: ?mkbyte(x)
Antworten: 8
Zugriffe: 1240

Re: ?mkbyte(x)

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 .
von Christoph Walther
8. Jan 2008 19:12
Forum: Archiv
Thema: Verifun download funktioniert nicht.
Antworten: 3
Zugriffe: 444

Re: Verifun download funktioniert nicht.

Hi, ich würde gern verifun für ein anderes Betriebsystem runterladen. Leider versagt aber seit 3 wochen der download server. Bzw wenn eine anwort kommt, dann heißt es immer "Übertragungsfehler" [antwort kommt vom verifunserver, nicht von meinem provider...]. Zum einen hätten Sie sich dann schon vor...
von Christoph Walther
20. Dez 2007 00:43
Forum: Archiv
Thema: probleme mit verifun
Antworten: 26
Zugriffe: 5545

if{?succ(y1), if{?succ(x1), if{half(x1) = half(y1), if{even(x1), if{pred(x1) = pred(y1), true, ¬ even(y1)}, if{pred(x1) = pred(y1), true, even(y1)}}, true}, true}, true} Also ich kann mich Baerchen nur anschließen. Bei mir hängt er sich am selben Schritt auf. Angenommen, 'half' ist injektiv. Mit 'h...
von Christoph Walther
19. Dez 2007 19:29
Forum: Archiv
Thema: Funktion wird graud
Antworten: 5
Zugriffe: 1174

Jup liegt am verschachtelten byte-add ... das gleiche hatte ich auch =) Nur zur klarstellung: VeriFun kann auch mit geschachtelten rekursionen umgehen. Beispiel: function g(x : nat) : nat <= if ?0(x) __then 0 __else if x > g(pred(x)) _______then g(g(pred(x))) _______else * ______end_if end_if lemma...

Zur erweiterten Suche