Die Suche ergab 86 Treffer

von Christoph Walther
22. Mär 2012 18:09
Forum: Archiv
Thema: Tips zur Nachklausur
Antworten: 0
Zugriffe: 704

Tips zur Nachklausur

1. Schauen Sie sich zuerst alle aufgaben an. 2. Beginnen Sie mit der aufgabe, die Ihnen am leichtesten erscheint. Danach die zweit-leichteste, usw. 3. Geben Sie sich eine maximalzeit vor, nach der Sie auf jeden fall zur nächsten aufgabe übergehen. 4. Wenn Sie zum schluß noch zeit haben, aber nur noc...
von Christoph Walther
20. Feb 2012 20:39
Forum: Archiv
Thema: Axiome aus Datentypdefinitionen, ?cons_i
Antworten: 2
Zugriffe: 334

Re: Axiome aus Datentypdefinitionen, ?cons_i

Wird ignoriert dass der Konstruktor succ einen Stuck-Term uebergeben bekommt, sodass einfach eq_{nat}(0, succ(\ldots)) \equiv false (Axiom 3) angewendet wird? Ja, genau so ist es. Denn für jeden nat -term t über der signatur eines (terminierenden!) L -programms gilt eq(0, succ(t)) = false mit axiom...
von Christoph Walther
13. Feb 2012 22:23
Forum: Archiv
Thema: Induktion
Antworten: 2
Zugriffe: 330

Re: Induktion

Hallo, ich habe zwei Fragen zu Induktionsaufgaben. 1) Muss bei HPL-Sequenzen in der Menge der Induktionshypothesen der Allquantor über die benutzten Variablen angegeben werden? Ja sicher. Es ist ja ein unterschied, ob man einen schrittfall der form ∀ x, y: ℕ x ≠ 0 ∧ φ[x - 1, y] → φ[x, y] oder der f...
von Christoph Walther
13. Feb 2012 00:30
Forum: Archiv
Thema: Axiome in der Klausur
Antworten: 9
Zugriffe: 884

Re: Axiome in der Klausur

Wenn in der Klausur gefordert ist, dass man die verwendeten Axiome in jedem Schritt angeben soll (wie in den Übungen), müsste man dann die Axiome ausschreiben? Bzw. am Anfang mit Nummern hinschreiben und dann per Nummer referenzieren? Wenn die antwort auf solch eine frage nicht aus der aufgabenstel...
von Christoph Walther
10. Feb 2012 23:21
Forum: Archiv
Thema: Axiome in der Klausur
Antworten: 9
Zugriffe: 884

Re: Axiome in der Klausur

Dh wir muessen wissen welche Axiome wir nutzen koennen, aber nicht die genauen Nummern das Axiome, oder? In einer akademischen prüfung werden wissen und fähigkeiten geprüft. Daran sollten Sie sich bei Ihren prüfungsvorbereitungen orientieren. Beispielsweise ist die nummerierung der axiome völlig wi...
von Christoph Walther
28. Jan 2012 16:30
Forum: Archiv
Thema: Hausübung 4 - Teil 2
Antworten: 3
Zugriffe: 561

Re: Hausübung 4 - Teil 2

Hallo, in der Aufgabestellung von 4.3 (c) heißt es, dass man für Axiome der Datentypen die Bezeichnungen (1)(a) bis (5)(a) wie auf Folie 3, Kapitel 9 verwenden soll. Für polymorphe Listen wird auf Folie 12, Kapitel 9 aber zwischen (5)(a1) und (5)(a2) unterschieden. Reicht es bei Anwendung einer die...
von Christoph Walther
24. Jan 2012 11:20
Forum: Archiv
Thema: Hausübung 4, Aufgabe 2
Antworten: 7
Zugriffe: 659

Re: Hausübung 4, Aufgabe 2

Hallo, viele Dank erstmal für die ausführliche Antwort, 2 Fragen stellen sich mir dann aber noch: 1. Steht das nicht im Gegensatz zu der Antwort von dschneid? Oder habe ich diese falsch interpretiert? 2. Könnten sie nochmal Bezug zu meinem zweiten Post nehmen, was ist die genaue Bedingung damit die...
von Christoph Walther
23. Jan 2012 20:56
Forum: Archiv
Thema: Hausübung 4, Aufgabe 2
Antworten: 7
Zugriffe: 659

Re: Hausübung 4, Aufgabe 2

Wenn ich mehrere Maßterme habe (z.B.: max(x, y) und min(x, y)), ist es dann zwingend notwendig, dass der erste Maßterm im (ersten) rekursiven Aufruf unter den gegebenen Bedingungen ein ">" liefert ... Ja. Zum beispiel kann die terminierung von function f(x : ℕ, y : ℕ) : ℕ <= if x > y then f(⁻(x), ⁺...
von Christoph Walther
7. Jan 2012 16:09
Forum: Archiv
Thema: DavisPutnam is sound
Antworten: 16
Zugriffe: 1625

Re: DavisPutnam is sound

Danke erstmal für die Hilfestellung, allerdings hänge ich immernoch am Anfang der dritten Aufgabe. Ich scheine weder zu verstehen, was du mit "als Referenz nutzen" meinst (im gegebenen Zusammenhang), noch inwiefern Sigma um Literale erweitert wird. Mir fehlt einfach der Ansatzpunkt. Ich habe die 5 ...
von Christoph Walther
6. Jan 2012 14:30
Forum: Archiv
Thema: Praktikum 3 - "DavisPutnam is complete"
Antworten: 21
Zugriffe: 1388

Re: Praktikum 3 - "DavisPutnam is complete"

Es ist doch ziemlich bemerkenswert, was diese Voraussetzungen machen, danke für den Tip. Bei einem Lemma (es verwendet als Variable die Liste S) habe ich die Voraussetzung ?::(S) mal entfernt, und plötzlich konnte das System das Lemma ohne Hilfe beweisen. Mit der Voraussetzung gab's anscheinend kei...
von Christoph Walther
5. Jan 2012 12:27
Forum: Archiv
Thema: Praktikum 3 - "DavisPutnam is complete"
Antworten: 21
Zugriffe: 1388

Re: Praktikum 3 - "DavisPutnam is complete"

Interessanterweise waren alle Lemmata bis auf eines schon vorhanden, nur Verifun hat sie nicht angewendet. Erst beim X. ten Versuch und einem Klick auf "Purge" ging es... Wenn ein lemma fehlt, kann das schon entscheidend sein für die automatische anwendung aller erforderlichen lemmata sein. In unse...
von Christoph Walther
25. Dez 2011 15:16
Forum: Archiv
Thema: Hausübung 3.2 a - Tippfehler?
Antworten: 1
Zugriffe: 435

Re: Hausübung 3.2 a - Tippfehler?

Sie haben recht, das ist ein schreibfehler.
von Christoph Walther
21. Dez 2011 19:03
Forum: Archiv
Thema: Anmeldung zur Pruefung im TuCan
Antworten: 11
Zugriffe: 1452

Re: Anmeldung zur Pruefung im TuCan

... bin am Überlegen, ob ich dann FGdI 3 lieber am 2. Termin schreiben sollte. Bevor ich mir mehr Gedanken drüber mache... darf ich das? Dabei sollte Sie (und andere) aber noch folgendes bedenken: Wenn Sie zum ersten mal die FGdI 3 - klausur am 2. termin schreiben und nicht bestehen, so ist die ers...
von Christoph Walther
2. Dez 2011 23:49
Forum: Archiv
Thema: 2.2.d
Antworten: 5
Zugriffe: 539

Re: 2.2.d

Hallo, sitzen jetzt schon eine Zeit lang daran und versuchen das Hilfslemma dbl(x) 6= succ(dbl(y)) zu beweisen. Haben schon viele Lemmata ausprobiert. :( Kann uns vielleicht jemand einen tipp geben ? Danke Lemma "lemma dbl_lemma <= ∀ x, y : ℕ¬ dbl(x) = ⁺(dbl(y))" eingeben und dann den Verify button...
von Christoph Walther
2. Dez 2011 20:13
Forum: Archiv
Thema: byte2nat is injective wfbyte
Antworten: 8
Zugriffe: 660

Re: byte2nat is injective wfbyte

Allgemeine Tipps: - bei vielen "if ??? then true else ..."-Kaskaden mit "Insert Hyptheses" vereinfachen Der tip is gut, damit werden beweisziele übersichtlicher. Aber besser erst mal mit Case Analysis arbeiten als mit Insert Hypotheses . Die in beiden fällen entstehenden sequenzen sind äquivalent, ...

Zur erweiterten Suche