Die Suche ergab 86 Treffer

von Christoph Walther
19. Dez 2007 11:06
Forum: Archiv
Thema: probleme mit verifun
Antworten: 26
Zugriffe: 5545

baerchen hat geschrieben:** sollte allerdings durchaus richtig sein, es gelten ja noch die hypothesen von oben
Die hypothesen hatte ich beim test übersehen.
von Christoph Walther
19. Dez 2007 02:14
Forum: Archiv
Thema: nicht evaluierbare statements
Antworten: 6
Zugriffe: 1639

das stimmt dass verifun solche ausdrücke nur erzeugt, wenn vorher festgestellt ist, dass ?+(-(-(x))), allerdings hatte ich gehofft die basisfälle ignorieren zu können (zb aus dem grund das -0 einfach nicht positiv ist), da lemmata mit vorbedingungen zwar korrekt evaluiert werden, aber ich sie nicht...
von Christoph Walther
19. Dez 2007 01:54
Forum: Archiv
Thema: probleme mit verifun
Antworten: 26
Zugriffe: 5545

Und das das Lemma: lemma unequal_nat2byte <= all x, y : nat if{¬ nat2byte(x) = nat2byte(y), ¬ x = y, true} Soll ausdrücken nat2byte(x) != nat2byte(y) -> x != y Dieses lemma ist unbrauchbar, da es keine spezifische aussage über die prozedur 'nat2byte' trifft. Das lemma hat die form: "¬ nat2byte(x) =...
von Christoph Walther
18. Dez 2007 20:47
Forum: Archiv
Thema: nicht evaluierbare statements
Antworten: 6
Zugriffe: 1639

Das Problem ist, dass der Beweiser diese Fälle von selbst findet in dem er aus irgendwelchen gründen im lauf der induktion x durch pred(x) ersetzt und das lemma das wir als übungsaufgabe beweisen sollen kann ich ja schlecht durch zusatzbedingungen einschränken edit: es liegt wohl an der prozedur ha...
von Christoph Walther
16. Dez 2007 18:22
Forum: Archiv
Thema: Praktische Hausübung 3
Antworten: 11
Zugriffe: 3767

Re: Praktische Hausübung 3

Ich habe Assoziativität, Kommutativität und Injektivität für die Addition und die Multiplikation der natürlichen Zahlen bewiesen. "Injektivität " haben Sie bestimmt nicht beweisen können, denn weder addition noch multiplikation sind injektiv: "plus" mit maus selektieren, im kontextmenue "Generate L...
von Christoph Walther
15. Dez 2007 17:41
Forum: Archiv
Thema: problem bei laden einer verifun datei
Antworten: 2
Zugriffe: 797

Re: problem bei laden einer verifun datei

Noch ein Problem: Beim Speichern bekomme ich folgende Fehlermeldung: VeriFun reported on Dec 15, 2007 1:18:11 PM: Error Unable to write to "[filename].vf": Not allowed to write a rule system different from TOP and NORMAL. Please prune truncated evaluations and try again. (java.io.InvalidClassExcept...
von Christoph Walther
15. Dez 2007 13:34
Forum: Archiv
Thema: problem bei laden einer verifun datei
Antworten: 2
Zugriffe: 797

Re: problem bei laden einer verifun datei

Die datei ist tatsächlich nicht lesbar. Warum, kann man nicht feststellen. Entweder wurde die datei von einem anderen programm verändert, oder es liegt ein bug von VeriFun beim schreiben oder lesen der datei vor - das wäre aber sehr ungewöhnlich, jedoch vollständig ausschließen kann man das nicht. U...
von Christoph Walther
12. Dez 2007 12:12
Forum: Archiv
Thema: probleme mit verifun
Antworten: 26
Zugriffe: 5545

hab probleme mit der ersetzung in negierten formeln. Man kann nicht erkennen, was in dem beispiel gegeben ist und was gezeigt werden soll. Also einfach die definitionen der verwendeten prozeduren und lemmata mit dem 'Copy' befehl aus dem Program Menue kopieren und in das posting pasten. Dazu das le...
von Christoph Walther
12. Dez 2007 12:05
Forum: Archiv
Thema: Dritte praktische Übung online
Antworten: 4
Zugriffe: 1007

Was habe ich vergessen ? Was muss ich beachten ? Fall 1: Die implementierung stimmt (trotz erfolgreicher tests) nicht. Dann haben Sie einfach nur mit eingaben getestet, die bei denen der fehler nicht auftritt. Fall 2: Die implementierung ist korrekt, so daß die zu beweisende aussage auch stimmt. Da...
von Christoph Walther
10. Dez 2007 23:21
Forum: Archiv
Thema: probleme mit verifun
Antworten: 26
Zugriffe: 5545

ok im handbuch und insbesondere in den codebeispielen des tutorial stehts eben anders Stimmt - beide sind für eine frühere systemversion geschrieben worden, aber wir haben bisher nicht die zeit für eine überarbeitung gefunden. Die sprachsyntax wurde geändert, dafür gibt es aber eine aktuelle beschr...
von Christoph Walther
16. Nov 2007 20:00
Forum: Archiv
Thema: Ernsthaftigkeit der Vorlesung...
Antworten: 11
Zugriffe: 2226

Der vorwurf, ich wiederspräche mich mindestens 10x je vorlesung ist eine behauptung, die unzutreffend ist und deshalb in dem posting auch unbelegt bleibt. Ausgangspunkt des postings ist ein fehler, den ich in der vorlesung vom 30.10. bei umformung einer formel in einem rechenbeispiel gemacht habe (i...
von Christoph Walther
8. Jun 2007 18:26
Forum: Archiv
Thema: Beispiel 12.4 (Turingmaschine)
Antworten: 0
Zugriffe: 1145

Beispiel 12.4 (Turingmaschine)

In der vorlesung wurde von einem studenten behauptet, daß die Turingtafel im beispiel unvollständig ist (7 zustände x 3 zeichen = 21 einträge). Dies ist ein irrtum: Die übergangsfunktion delta ist nur auf zuständen =/ endzustand definiert, vgl. Definition 12.1. Damit erhält man 6 zustände x 3 zeiche...
von Christoph Walther
2. Jun 2007 20:36
Forum: Archiv
Thema: Aufgabe 6.3 h,i
Antworten: 4
Zugriffe: 1348

Re: Aufgabe 6.3 h,i

Hallo, ich habe einpaar ganz kleine Fragen an die Aufgabe 6.3 h und i. In Aufgabe h, ist die Anzahl der Eingabeparameters der Funktion "nuy-b-h" (1 + k), mit k: Dimensionen des Vektor x. Wenn die frage ist, ob das stimmt, so lautet die antwort 'ja'. In Aufgabe i, Die Funktion half(x) wird durch die...
von Christoph Walther
2. Jun 2007 20:28
Forum: Archiv
Thema: Aufgabe 6.3 h,i
Antworten: 4
Zugriffe: 1348

tm_n hat geschrieben:Für die Aufgabe 6.3.h,

wie wird die Funktion "nuy-b-h" definiert, wenn es mehrere m gibt, und es gilt m < n, und f(m,V(x)) =0?

V(x) steht für Vector x.
Nehmen Sie das kleinste 'm' mit m < n und f(m, x*)=0.

cw.

PS: Aussprache nicht 'nuy' sondern 'müh'.
von Christoph Walther
2. Jun 2007 20:09
Forum: Archiv
Thema: Frage zur Reduktion der leeren Menge...
Antworten: 3
Zugriffe: 1990

Re: Frage zur Reduktion der leeren Menge...

CloneCommander hat geschrieben:Mir hat nun jemand gesagt, die Funktion solle total und berechenbar sein
'Jemand' hat recht - für die reduktionsfunktion fordert man 'berechenbar' und 'total'. Das skript ist hier fehlerhaft (sorry) & muß diesbzgl. korrigiert werden.

cw.

Zur erweiterten Suche