Die Suche ergab 15 Treffer

von wintermute
30. Okt 2017 15:54
Forum: Archiv
Thema: SBT Submission only possible from interactive console
Antworten: 5
Zugriffe: 662

Re: SBT Submission only possible from interactive console

mirko-koehler hat geschrieben:
30. Okt 2017 15:03
Make sure to use quotation marks when running sbt in batch mode, i.e.

Code: Alles auswählen

sbt "submit <tu-id> <token>"
works for me.


Mirko
I have just tried it. Using quotation marks does the trick for me.

Thanks mirko-koehler and 0b101101101 for your help.
von wintermute
30. Okt 2017 14:20
Forum: Archiv
Thema: SBT Submission only possible from interactive console
Antworten: 5
Zugriffe: 662

SBT Submission only possible from interactive console

Hi all, I had problems with the submission of my solution of assignment 0. After some experimenting I have found out that the submit task only works from the interactive sbt console for me. If I type the following directly into my command prompt sbt submit <tu-id> <token> I get this error [error] [e...
von wintermute
7. Mär 2017 18:38
Forum: Archiv
Thema: Beweis: while true terminiert nicht (-> neue Übungsaufgabe)
Antworten: 5
Zugriffe: 589

Re: Beweis: while true terminiert nicht

Hallo, per Widerspruchsbeweis wird in den Folien gesagt, dass "while true do skip od" nicht terminiert, da der Zustand nach einem Schleifendurchlauf wieder der selbe ist. Wie würde man Beweisen, dass "while true do c od" nie terminiert? Man kann dann nicht sagen, dass o=o', wodurch man den Widerspr...
von wintermute
7. Mär 2017 15:56
Forum: Archiv
Thema: Programmäquivalenz
Antworten: 2
Zugriffe: 473

Re: Programmäquivalenz

Kann ich das anhand von Einsetzen zeigen oder argumentiere ich einfach, das x im Zustand o'' zu 0 ausgewertet wird? Nur ganz kurz, du musst schon das Urteil \langle(x \oplus 1), \sigma''\rangle \Downarrow 1 herleiten. Das wird schließlich in der Prämisse der Regel r:= benötigt. Dort möchtest du, ja...
von wintermute
7. Mär 2017 15:37
Forum: Archiv
Thema: Traces P;Q
Antworten: 1
Zugriffe: 328

Re: Traces P;Q

Gilt dann nach diesem Teil der Definition für: \{ s.t \space | \space s.(\checkmark) ∈ traces(P) ∧ t ∈ traces(Q)\} = \{ ((), \checkmark), (x, \checkmark) \} ? Das gilt nicht. Nehmen wir beispielsweise (x, \surd) \in \{s.t \space | \space s.(\surd) ∈ traces(P) ∧ t ∈ traces(Q)\} an. Es gibt jetzt dre...
von wintermute
7. Mär 2017 15:13
Forum: Archiv
Thema: Konvention Tupel-Dekomposition
Antworten: 0
Zugriffe: 279

Konvention Tupel-Dekomposition

Hallo, wir haben in Modul 1 auf Folie 15 das kartesische Produkt auf endlichen Folgen eingeführt. (Ich möchte an dieser Stelle anmerken, dass hier das intuitive Verständnis von endlichen Folgen vorausgesetzt wird, da endliche Folgen selber erst auf Folie 17 auf Basis der Definition von Folie 15 eing...
von wintermute
7. Mär 2017 15:07
Forum: Archiv
Thema: Wohlfundierte Relation auf Herleitungen
Antworten: 6
Zugriffe: 916

Re: Wohlfundierte Relation auf Herleitungen

Ich glaube, mein Problem ist, dass ich nicht verstehe, wieso die Herleitung von while true do skip od endlich ist. Ich kann doch bis in alle Ewigkeit rwht anwenden, oder nicht? Natürlich ist das möglich, dennoch ist jede Herleitung selbst endlich lang. Um es hoffentlich etwas klarer zu machen: Es l...
von wintermute
7. Mär 2017 14:21
Forum: Archiv
Thema: Wohlfundierte Relation auf Herleitungen
Antworten: 6
Zugriffe: 916

Re: Wohlfundierte Relation auf Herleitungen

Hallo, ich verstehe nicht ganz, warum die in Modul 7, Folie 11 definierte Relation für Com wohlfundiert ist. Existiert hier nicht ein ähnliches Problem wie bei der Strukturellen Induktion, nämlich, dass es bei der while-Schleife nicht unbedingt ein "kleinstes" Element gibt, denn die rwht-Regel könn...
von wintermute
3. Mär 2017 16:20
Forum: Archiv
Thema: Aufgabe 1.2
Antworten: 2
Zugriffe: 174

Re: Aufgabe 1.2

In der Musterlösung wird diese Anordnung in der Definition der Menge REIHE erzwungen. Die prädikaktenlogischen Formel hat folgende Form: (\forall k \in h: \varphi_1 \vee \varphi_2) \wedge \varphi_3 \vee \varphi_4 \varphi_1 := (\exists k' \in h: \text{num-wert}(\text{wert}(k')) = \text{num-wert}(\tex...
von wintermute
28. Feb 2017 12:43
Forum: Archiv
Thema: Lerngruppe zur Diskussion von eigenen Lösungen gesucht
Antworten: 6
Zugriffe: 417

Re: Lerngruppe zur Diskussion von eigenen Lösungen gesucht

Hallo, ich freue mich über das Interesse. Gerne können wir auch via Messenger diskutieren Über Messenger finde ich auch eine Superidee. Ich bin da 100% dabei Die Idee finde ich gut. Bisher gibt es noch keine Messenger-Gruppe, aber ich werde heute eine Skype-Gruppe erstellen. Schreibt mir am Besten e...
von wintermute
18. Feb 2017 22:45
Forum: Archiv
Thema: Lerngruppe zur Diskussion von eigenen Lösungen gesucht
Antworten: 6
Zugriffe: 417

Lerngruppe zur Diskussion von eigenen Lösungen gesucht

Hallo, in Vorbereitung auf die Klausur suche ich Interessierte für eine Lerngruppe. Das Ziel der Lerngruppe soll nicht das gemeinsame Bearbeiten von Aufgaben in Präsenz sein. Ich bin der Meinung, dass der Lerneffekt dann am höchsten ist, wenn jeder die Aufgaben für sich selbst löst. Stattdessen soll...
von wintermute
10. Jul 2016 15:08
Forum: AuD: Theoretische Aufgaben
Thema: [BFS] Inhalt der Variante
Antworten: 6
Zugriffe: 500

Re: [BFS] Inhalt der Variante

Danke für die schnelle Antwort. Ich glaube jetzt habe ich es verstanden. Ich wollte mit folgenden Satz: Wenn man zulässt, dass die Variante Änderungen an Variablen nur unvollständig beschreiben darf wie hier im Fall bei der FIFO queue Q , benötigt man weitere Voraussetzungen um die Terminierung zu b...
von wintermute
10. Jul 2016 12:02
Forum: AuD: Theoretische Aufgaben
Thema: [BFS] Inhalt der Variante
Antworten: 6
Zugriffe: 500

Re: [BFS] Inhalt der Variante

Danke für die Antworten. Mir ist klar geworden, wie die Terminierung des Algorithmus gezeigt werden kann. Mein Problem war die Annahme, dass die Variante als alleinige Voraussetzung genügen soll (neben den impliziten allgemein üblichen Annahmen und Definitionen), um die Terminierung zu beweisen: Var...
von wintermute
6. Jul 2016 21:08
Forum: AuD: Theoretische Aufgaben
Thema: [BFS] Inhalt der Variante
Antworten: 6
Zugriffe: 500

Re: [BFS] Inhalt der Variante

Das beantwortet meine Frage teilweise. Ich kann nachvollziehen, dass Änderungen an Variablen, die keinen Einfluss auf die Abbruchbedingung haben, für den Korrektheitsbeweis unerheblich sind. Im gegebenen Fall ist die Abbruchbedingung " Q = \emptyset ." Das heißt sie hängt von der Variable Q ab. In d...
von wintermute
6. Jul 2016 13:44
Forum: AuD: Theoretische Aufgaben
Thema: [BFS] Inhalt der Variante
Antworten: 6
Zugriffe: 500

[BFS] Inhalt der Variante

Hallo, mir ist beim Lesen des Wiki-Eintrags zur Breitensuchen (Breadth-first search) aufgefallen, dass dort als Variante One node is removed from Q . gewählt wurde. Nun wird im Abschnitt "Induction step" beschrieben, was innerhalb einer Iteration passiert: Extract the first element v from Q . Append...

Zur erweiterten Suche