Die Suche ergab 86 Treffer

von Christoph Walther
1. Feb 2010 23:56
Forum: Archiv
Thema: HA 4.1 e)
Antworten: 5
Zugriffe: 695

Re: HA 4.1 e)

-me- hat geschrieben:Darf man annehmen, dass so etwas wie hd(5 :: k) = 5 und succ(x + y) > x + y <=> 1 > 0 <=> true gilt ?
Ja.
von Christoph Walther
27. Jan 2010 10:49
Forum: Archiv
Thema: Wieviele Semesterwochenstunden?
Antworten: 4
Zugriffe: 485

Re: Wieviele Semesterwochenstunden?

nieswand hat geschrieben:hat jemand eine Ahnung, wieviele Semesterwochenstunden man sich für die bestandene FGdI3-Prüfung anrechnen lassen kann?
2 (Vorlesung) + 1 (Übung) + 1(Praktikum) = 2 + 2 SWS.
von Christoph Walther
21. Jan 2010 13:43
Forum: Archiv
Thema: Relationenbeschreibung einer Prozedur
Antworten: 3
Zugriffe: 322

Re: Relationenbeschreibung einer Prozedur

mister_tt hat geschrieben:Gut. Und die atomare Relationenbeschreibung für ("f(f(pred(x)))") enthält einmal die Substitution x/f(pred(x)) und die Substitution x/pred(x) oder nur eins von beiden? Da bin ich noch etwas verwirrt...
Dann orientieren Sie sich doch einfach an Definition 5 in Kapitel 7.
von Christoph Walther
7. Jan 2010 14:41
Forum: Archiv
Thema: Hilfe zur 3.3
Antworten: 7
Zugriffe: 673

Re: Hilfe zur 3.3

Hallo Peter Anscheinend hast du ja verstanden, wie man die Induktionshypothesen benutzt. Was genau soll man denn da betrachten? Die Einträge unter dem Reiter "Hypotheses" oder unter "Induction Hypotheses"? Und wie wendet man die an? Bzw wiebenutzt man "Insert Induction Hypotheses"? Was und wie gibt...
von Christoph Walther
13. Dez 2009 17:42
Forum: Archiv
Thema: Farben im Proofviewer
Antworten: 4
Zugriffe: 263

Re: Farben im Proofviewer

Laut diesen Changelogs von VeriFun sind dunkle Farben (grün/rot) aufjedenfall zu beweisen/wiederlegen und die helleren Farben grün/rot könnten als alternative bewiesen oder wiederlegt werden. Wobei rot immer wiederlegen heisst und grün beweisen. Das stimmt aber nur, solange "Highlight terms to prov...
von Christoph Walther
10. Dez 2009 20:01
Forum: Archiv
Thema: [P3] Funktion mother?
Antworten: 1
Zugriffe: 317

Re: [P3] Funktion mother?

Die datenstruktur 'term' ist durch gegenseitige rekursion definiert: term -> list[term] -> term. In vf3.2.2 kann die fundiertheit der strukturellen ordnung von gegenseitig rekursiv definierten datenstrukturen nicht bewiesen werden. Also muß man dies dem system als eine art axiom mitteilen. Dies gesc...
von Christoph Walther
7. Dez 2009 20:28
Forum: Archiv
Thema: Matching f(x)=a
Antworten: 3
Zugriffe: 228

Re: Matching f(x)=a

Gibt es einen Matcher für t=f(x) und q=a? Mit dem Kalkül kann man keine Regel anwenden, also gibt es keinen Matcher. Korrekt. Aber könnte man nicht x/f^-1(a) ersetzen, falls f^-1 existieren würde? Ja schon, wenn es denn so wäre. Dann würde man unter einer Gleichheitstheorie matchen. Die theorie wär...
von Christoph Walther
3. Dez 2009 11:53
Forum: Archiv
Thema: "Vererbung" / Weiterleitung von Exceptions
Antworten: 2
Zugriffe: 254

Re: "Vererbung" / Weiterleitung von Exceptions

mister_tt hat geschrieben:Was ist nun richtig?
Die antwort findet man auf folie 5/21 - schauen Sie sich das noch mal genau an.
von Christoph Walther
30. Okt 2009 23:38
Forum: Archiv
Thema: Wofür Hilfslemma für sumlist(myList, 0)=sum(myList)?
Antworten: 2
Zugriffe: 404

Re: Wofür Hilfslemma für sumlist(myList, 0)=sum(myList)?

glowhand hat geschrieben: Ich würde gerne wissen, warum Verifun nicht in der Lage ist, sumlist(Liste, 0) = sum(Liste) zu beweisen.
Mit VeriFun hat das nichts zu tun. Versuchen Sie doch einfach diese behauptung selbst ohne hilfslemma zu beweisen. Dann erkennen Sie das problem, um das es hier geht.
von Christoph Walther
14. Okt 2009 13:10
Forum: Archiv
Thema: Verifun unter Windows 7
Antworten: 11
Zugriffe: 1366

VeriFun & JAVA

Einen der gründe zur vorgeschriebenen verwendung von JAVA 1.5 findet man in http://verifun.org/ unter "Bugs". Nach unserer erfahrung ist mit einer neuen JAVA version nicht garantiert, daß das system noch fehlerfrei & effizient arbeitet. Dies betrifft vor allem die oberfläche, die lauftzeitperformanc...
von Christoph Walther
26. Mär 2009 13:30
Forum: Archiv
Thema: Tote Funktion in VeriFun
Antworten: 8
Zugriffe: 479

Re: Tote Funktion in VeriFun

Ich kann in VeriFun reproduzierbar eine Funktion anlegen, die ein graues Prozedur-Icon bekommt (VeriFun konnte also keine Maßterme erzeugen), bei der andererseits aber auch die Funktion "Set Termination" im Kontextmenü sowie im Hauptmenü deaktiviert ist. Die systemverhalten ist ok (also kein bug) &...
von Christoph Walther
26. Mär 2009 00:09
Forum: Archiv
Thema: Übung 4.4 a) b)
Antworten: 6
Zugriffe: 389

Re: Übung 4.4 a) b)

Wie beweißt man allgemein, dass eine Prozedur total ist? Muss man nicht erstmal beweißen, dass die Funktion für alle minimale Elemente definiert ist, und dann für alle nicht-minimale? Mal zur begriffsbildung: 1. Eine Funktion kann total (oder auch nicht total ) sein. 2. Eine Prozedur (und allgemein...
von Christoph Walther
25. Mär 2009 23:49
Forum: Archiv
Thema: VeriFun Axiome
Antworten: 4
Zugriffe: 412

Re: VeriFun Axiome

Stimmt schon. Aus dem Stand kann VeriFun das nich beweisen. Da wurde wohl beim erstellen der Aufgabe getrickst. NEIN & JA. NEIN, denn die terminierung von DP wurde ja mit VeriFun in Praxisübung 4 bewiesen. JA, da im beweisbaum nur 'true' steht. Erklärung: Es gibt in VeriFun einen mechanismus, durch...
von Christoph Walther
24. Mär 2009 00:50
Forum: Archiv
Thema: Wozu 2 Interpreter?
Antworten: 3
Zugriffe: 349

Re: Wozu 2 Interpreter?

So ist es. evalp dient vor allem dazu, die Semantik der Sprache zu definieren. Für das führen von Gleichheitsbeweisen ist er jedoch ungeeignet, da er nicht symbolisch mit Variablen rechnen kann. Anders gesagt: Mit evalP wird gerechnet. Z.B. "2+2" wird zu "4" ausgerechnet und "2+2=4" wird zu "true" ...
von Christoph Walther
24. Mär 2009 00:31
Forum: Archiv
Thema: Klausurbonus
Antworten: 2
Zugriffe: 337

Re: Klausurbonus

Falls Sie alle vier Testate erreichen, erhalten Sie einen Bonus von 0,3 Notenstufen für die Klausur. Außerdem erhalten Sie bei Erreichen von mindestens 75% der Punkte in den Hausübungen einen Bonus von 0,3 Notenstufen für die Klausur. (Ein Bonus von 0,3 Notenstufen bedeutet, dass Sie zum Beispiel s...

Zur erweiterten Suche