Die Suche ergab 271 Treffer

von dschneid
16. Jan 2012 21:33
Forum: Archiv
Thema: Orakel-Turingmaschine
Antworten: 6
Zugriffe: 914

Re: Orakel-Turingmaschine

Geht man davon aus, irgendwann einmal das Halteproblem lösen zu können und überlegt sich jetzt schon einmal was dann möglich wäre? Das Halteproblem wird nie lösbar sein. Da geht es nicht darum, dass noch kein Uber-Hacker den passenden Algorithmus gefunden hat: Man kann mathematisch beweisen, dass d...
von dschneid
9. Jan 2012 00:06
Forum: Archiv
Thema: Praktikum 3 - "DavisPutnam is complete"
Antworten: 21
Zugriffe: 1413

Re: Praktikum 3 - "DavisPutnam is complete"

Ich würde an deiner Stelle mal hingehen...
von dschneid
8. Jan 2012 23:38
Forum: Archiv
Thema: Praktikum 3 - "DavisPutnam is complete"
Antworten: 21
Zugriffe: 1413

Re: Praktikum 3 - "DavisPutnam is complete"

Wir reden von zwei verschiedenen Dingen: Ich meine die beiden Fälle, die man nach der Case Analysis im ersten Zweig erhät; du aber meinst die beiden Zweige in den verschiedenen Induktionsschritten. Du wirst vielleicht sehen, dass mein Goal ein Teil des ersten Terms ist, den du gepostet hast.
von dschneid
8. Jan 2012 19:52
Forum: Archiv
Thema: Praktikum 3 - "DavisPutnam is complete"
Antworten: 21
Zugriffe: 1413

Re: Praktikum 3 - "DavisPutnam is complete"

Das Problem ist hier, dass nicht alle Annahmen, die man in einem Lemma verwenden könnte, im Goal-Term stehen. Weitere Annahmen folgen aber aus der Induktionshypothese. Nehmen wir als Beispiel den ersten Fall; das Goal ist: if{?ø(hd(S)), true, if{DavisPutnam(split(∼(hd(hd(S))), tl(S))), true, if{Davi...
von dschneid
8. Jan 2012 13:33
Forum: Archiv
Thema: Praktikum 3 - "DavisPutnam is complete"
Antworten: 21
Zugriffe: 1413

Re: Praktikum 3 - "DavisPutnam is complete"

Mit der Case Analysis will man nur das eher große Goal in zwei kleinere, einfacher zu behandlende aufteilen. Man nimmt also als Case Term einfach die äußerste Bedingung des Goals.

Der Beweis funktioniert genauso gut ohne die Case Analysis; das soll es nur einfacher machen, die Sache zu überblicken.
von dschneid
7. Jan 2012 17:49
Forum: Archiv
Thema: DavisPutnam is sound
Antworten: 16
Zugriffe: 1731

Re: DavisPutnam is sound

Wobei das ganz interessant hier ist: Ich konnte ein Lemma beweisen, das aussagt, dass L und ~L nicht beide in einer Interpretation enthalten sein können; aber auch eines, das sagt, wenn L in einer Klausel enthalten ist, jede beliebige Interpretation L :: σ die Klausel erfüllt. Also insbesondere auc...
von dschneid
7. Jan 2012 02:06
Forum: Archiv
Thema: DavisPutnam is sound
Antworten: 16
Zugriffe: 1731

Re: DavisPutnam is sound

Dafür ist es ein bisschen spät; die Abgabe ist ja schon am Sonntag und dann geht es gleich mit den Testaten los. Vielleicht hier also einfach eine kleine Tele-Pool-Sprechstunde am Beispiel des ersten Teilbaumes von "DavisPutnam is sound": Um zum Erfolg zu kommen, kann man einen der grün markierten T...
von dschneid
4. Jan 2012 14:15
Forum: Archiv
Thema: Praktikum 3 - "DavisPutnam is complete"
Antworten: 21
Zugriffe: 1413

Re: Praktikum 3 - "DavisPutnam is complete"

Ganz im Gegenteil; sowohl DavisPutnam als auch \(\rho\) müssen eigentlich immer herausgeneralisiert werden.
von dschneid
16. Dez 2011 21:25
Forum: Archiv
Thema: Berechnungskalkül Abkürzen
Antworten: 2
Zugriffe: 505

Re: Berechnungskalkül Abkürzen

Ja, das ist erlaubt, allerdings nur, wenn der abgekürzte Ausdruck nicht später relevant wird. Es ist also beispielsweise so etwas wie \(if\{true, [Ausdruck], ...\}\) in Ordnung, aber \(if\{true, ..., [Ausdruck] \}\) nicht, weil dann der im nächsten Schritt behandelte Ausdrucks "aus dem Nichts" erscheint.
von dschneid
10. Dez 2011 21:06
Forum: Archiv
Thema: Hausübung 2 Aufgabe 2.2 a) Hinweis
Antworten: 5
Zugriffe: 402

Re: Hausübung 2 Aufgabe 2.2 a) Hinweis

Nein, denn 2 ist das Ergebnis von ^-(3) , während beispielsweise ^+(0) und 1 nur verschiedene Schreibweisen für dasselbe sind. Letzteres ist nur eine notationelle Abkürzung, mit der anderen "Abkürzung" würdest du dagegen Schritte im Berechnungskalkül überspringen (nämlich für die Anwendung des Selek...
von dschneid
9. Dez 2011 21:07
Forum: Archiv
Thema: Hausübung 2 Aufgabe 2.2 a) Hinweis
Antworten: 5
Zugriffe: 402

Re: Hausübung 2 Aufgabe 2.2 a) Hinweis

Du hast es genau verkehrt herum: succ ist ein Konstruktor, pred ist der dazugehörige Selektor. Mit succ "konstruierst" du eine um eins größere Zahl aus einer anderen, mit pred kannst du aus der konstruierten Zahl wieder die kleinere "selektieren". succ und pred alleine sind weder Konstruktorgrundter...
von dschneid
7. Dez 2011 20:26
Forum: Archiv
Thema: Ort der Testate?
Antworten: 2
Zugriffe: 248

Re: Ort der Testate?

C-Pool.
von dschneid
5. Dez 2011 14:22
Forum: Archiv
Thema: Shapereader
Antworten: 5
Zugriffe: 482

Re: Shapereader

Der vector speichert Pointer auf FiniteShapes. Deswegen brauchst du von Triangle t die Adresse, also fügst du &t in den vector ein.
von dschneid
3. Dez 2011 10:02
Forum: Archiv
Thema: Übung 3 Aufgabe 4
Antworten: 3
Zugriffe: 231

Re: Übung 3 Aufgabe 4

Du musst du Fallunterscheidung ja nicht unbedingt im Kalkül machen, sondern kannst einfach auf der Metaebene zwei Fälle behandeln.
von dschneid
1. Dez 2011 21:45
Forum: Archiv
Thema: ex05 aufgabe 1.a
Antworten: 2
Zugriffe: 388

Re: ex05 aufgabe 1.a

Mit Beweisen hat das ja erstmal gar nichts zu tun. Gelb heißt, die Zeile wurde nicht ganz ausgeführt (genauer: nicht alle Bytecode-Instruktionen, zu denen die Zeile kompiliert wird, wurden ausgeführt). Das passiert, wenn du in deinen Tests immer im ersten Durchlauf schon durch das break abbrichst un...

Zur erweiterten Suche