Protokoll

Prüfer: Daniel, Lutz. Fragen nur von Daniel

1. Antwort: Solved das Goal, wenn False im Kontext

1. Nachfrage: Was ist mit:

     H: x = 1
     ----------------------
     

1. Antwort: Geht net, nur mit inversion. contradiction will tatsächlich

False (oder (A ∧ ¬A))

1. Antwort: Induktiver Datentyp mit einem Konstruktor, der zwei Prämissen

nimmt.

1. Frage: Wie prooft man es?

1. Antwort: split oder apply vom Konstructor

1. Antwort:

1. Für expressions: Evaluieren auf das Gleiche
2. Für statements: Genau dann wenn das Eine mit state x terminiert, tuts

das andere auch.

1. Hab skip, seq, if und while hingeschreiben, dann hat er gesagt, es passt schon

 Habe hingeschreben:

 #+BEGIN_EXAMPLE
 { y = n }
 X := 1;
 while (y > 0) then
   x := y * x; y := y - 1
 end
 { x = n! }
 #+END_EXAMPLE

 Anwenden: Seq, Assign, Consequence, While

 Nachdem ich mit consequence die invariante hatte, hat er abgebrochen.

1. Programm auf einmal komplett evaluieren vs. einzelne Evaluationsschritte

 Implementierung von Parallel-Imp