Instituts-Logo Logik in der Informatik
Prof. Dr. Nicole Schweikardt
Humboldt-Logo

Logbuch zur Vorlesung Logik in der Informatik

Wintersemester 2014/15

Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, die in der Vorlesung verwendeten Folien, Teile des Skripts und gelegentlich auch Korrekturen und sonstige ergänzende Bemerkungen.


  1. Mi, 15.10.2014:   Folien 1-29

    Kapitel 1: Einführung ins Thema "Logik in der Informatik" - Paradoxien, Syllogismen, Anwendungen der Logik in der Informatik.
    Organisatorisches (entlang der Webseite der Vorlesung).
    Start mit Kapitel 2: Aussagenlogik - heute: Syntax der Aussagenlogik.

    Material: Folien, Skript zu Kapitel 1, Skript zu Kapitel 2 - Teil 1,
    Weitere Lektüre: Kapitel 1 und 2.A in [KK], Einleitung und Kapitel 1.1 in [S], Vorwort und Kapitel 1.1, 1.5 und 2.1 in [B].
    Eine Vorabversion des in der Vorlesung zitierten Artikel "On the unusual effectiveness of logic in computer science" von Halpern, Harper, Immerman, Kolaitis, Vardi und Vianu (Bulletin of Symbolic Logic 7(2):213-236 (2001)) finden Sie hier.

  2. Fr, 17.10.2014:   Folien 30-58

    Weiter mit Kapitel 2: Aussagenlogik - heute: Interpretationen, Semantik der Aussagenlogik, rekursive Definitionen über Formeln, Modelle, das Koinzidenzlemma, Wahrheitstafeln, ein Logikrätsel, computerlesbare Darstellung von Formeln, Demo des Formelcheckers für die Aussagenlogik "(tks.AL)", Auflösung des Rätsels zur Geburtstagsfeier (Beispiel 2.1), Erfüllbarkeit, Allgemeingültigkeit, die Folgerungsbeziehung.

    Material: Folien, Skript zu Kapitel 2 - Teil 2, Formelchecker für die Aussagenlogik: (tks.AL)
    Weitere Lektüre: Kapitel 1 und 2.A in [KK], Einleitung und Kapitel 1.1 in [S], Kapitel 2.1 und 2.2 in [B].

  3. Mi, 22.10.2014:   Folien 59-82

    Weiter mit Kapitel 2: Aussagenlogik - heute: die Folgerungsbeziehung; Modus Ponens; Zusammenhänge zwischen Allgemeingültigkeit, Erfüllbarkeit und Folgerungsbeziehung; aussagenlogische Modellierung am Beispiel von Sudokus und automatischer Hardwareverifikation; Äquivalenz von Formeln und Formelmengen; fundamentale Äquivalenzen

    Material: Folien, Skript zu Kapitel 2 - Teil 3, Übungsblatt 1
    Weitere Lektüre: Kapitel 1 und 2.A in [KK], Kapitel 1.1 und 1.2 in [S], Kapitel 2.2 in [B].

  4. Fr, 24.10.2014:   Folien 83-99

    Weiter mit Kapitel 2: Aussagenlogik - heute: der Dualitätssatz; Beweise per Induktion über den Aufbau von Formeln; boolesche Funktionen und Vollständigkeit der Aussagenlogik; Adäquatheit von Mengen von Junktoren und Konstanten; exklusives Oder, der Mehrheitsjunktor und der Sheffer-Strich; Negationsnormalform (NNF)

    Material: Folien, Skript zu Kapitel 2 - Teil 4
    Weitere Lektüre: Kapitel 2.A in [KK], Kapitel 1.1 und 1.2 in [S], Kapitel 2.4.1 und 2.5 in [B].

  5. Mi, 29.10.2014:   Folien 100-112

    Weiter mit Kapitel 2: Aussagenlogik - heute: ein Beispiel zur Transformation in NNF; DNF und KNF; eine kleine Formel mit großer DNF; der Endlichkeitssatz

    Material: Folien, Skript zu Kapitel 2 - Teil 5, Übungsblatt 2
    Weitere Lektüre: Kapitel 2.A in [KK], Kapitel 1.2 und 1.4 in [S], Kapitel 2.6 und 2.8 in [B].

  6. Fr, 31.10.2014:   Folien 111-119

    Weiter mit Kapitel 2: Aussagenlogik - heute: Abschluss des Beweises des Endlichkeitssatzes; Beispiel für eine Anwendung des Endlichkeitssatzes (um nachzuweisen, dass ein unendlicher Graph genau dann k-färbbar ist, wenn jeder endliche Subgraph k-färbbar ist); einführendes Beispiel zum Thema Resolution; Tseitin-Verfahren zur effizienten Umwandlung beliebiger Formeln in erfüllbarkeitsäquivalente KNF-Formeln; Repräsentation disjunktiver Klauseln durch endliche Mengen von Literalen; Repräsentation von KNF-Formeln durch endliche Klauselmengen

    Material: Folien, Skript zu Kapitel 2 - Teil 6
    Weitere Lektüre: Kapitel 2.A und 2.B in [KK], Kapitel 1.4 und 1.5 in [S], Kapitel 2.8 und 2.10 in [B].

  7. Mi, 05.11.2014:   Folien 119-125

    Weiter mit Kapitel 2: Aussagenlogik - heute: der Begriff einer Resolvente zweier Klauseln; das Resolutionslemma; Resolutionsableitungen und Resolutionswiderlegungen; Korrektheit und Vollständigkeit der Resolution (Beginn des Beweises von Satz 2.61, der besagt, dass eine Klauselmenge genau dann eine Resolutionswiderlegung besitzt, wenn sie unerfüllbar ist)

    Material: Folien, Skript zu Kapitel 2 - Teil 7, Übungsblatt 3
    Weitere Lektüre: Kapitel 2.B in [KK], Kapitel 1.5 in [S], Kapitel 2.10 in [B].

  8. Fr, 07.11.2014:   Folien 126-136

    Weiter mit Kapitel 2: Aussagenlogik - heute: Abschluss des Beweises von Satz 2.61, der besagt, dass eine Klauselmenge genau dann eine Resolutionswiderlegung besitzt, wenn sie unerfüllbar ist; Vorsicht beim Anwenden der Resolutionsregel; der Satz von Haken (ohne Beweis); Algorithmen zur Lösung des (NP-vollständigen) aussagenlogischen Erfüllbarkeitsproblems: der Wahrheitstafelalgorithmus, der Resolutionsalgorithmus, der DPLL-Algorithmus (inkl. Beispiel)

    Material: Folien, Skript zu Kapitel 2 - Teil 8
    Weitere Lektüre: Kapitel 2.B in [KK], Kapitel 1.5 in [S], Kapitel 2.10 in [B].
    Die SAT Competition ist ein jährlich stattfindender internationaler Wettbewerb, bei dem effiziente Implementierungen von Algorithmen zur Lösung des SAT-Problems gegeneinander antreten. Mehr Details finden Sie auf der Webseite der SAT Competition 2014. Im Jahr 2014 fanden im Rahmen des Vienna Summer of Logic auch die FLoC Olympic Games 2014 statt, in die die SAT Competition 2014 eingebettet war.

  9. Mi, 12.11.2014:   Folien 137-144

    Abschluss von Kapitel 2: Aussagenlogik - heute: Hornklauseln und Hornformeln; der Streichungsalgorithmus: ein effizienter Erfüllbarkeitsalgorithmus für Hornformeln (Algorithmus, Beispiel-Läufe, Laufzeitanalyse und Korrektheitsbeweis)

    Material: Folien, Skript zu Kapitel 2 - Teil 8, Übungsblatt 4
    Weitere Lektüre: Kapitel 3.A und 3.B in [KK], Kapitel 1.3 in [S], Kapitel 2.11 in [B].

  1. Mi, 19.11.2014:   Folien 145-178

    Start mit Kapitel 3: Logik-Programmierung - heute: Einführung ins Thema ("deklarativ" vs. "imperativ") und Anwendungsgebiete der Logikprogrammierung; Syntax und Semantik von Logikprogrammen: Fakten, Anfragen, Variablen, Regeln, das Ungleichheitsprädikat, Atome, Zahlen, Konstanten, Terme, Substitutionen, Anwendung von Substitutionen, Instanzen von Termen, Grundterme und Grundinstanzen, Ableitungen aus Logikprogrammen, Beweisbäume, deklarative Semantik von Logikprogrammen: formale Definition der Bedeutung eines Programms und der Antwort auf eine Anfrage; viele Beispiele

    Material: Folien, Skript zu Kapitel 3 - Teil 1, Quelltext der Programme bibel1.pl, party1.pl, plus1.pl, plus2.pl, bibel2.pl, bibel3.pl, bibel4.pl, bibel5.pl
    Ein Übungsblatt wurde heute nicht ausgeteilt; das nächste Übungsblatt wird es nächsten Mittwoch (26.11.) geben.
    Weitere Lektüre: Introduction und Chapter 1 (Basic Constructs) in [SS], Kapitel 3.C in [KK], Kapitel 3.1 und 3.2 in [S]

  2. Fr, 21.11.2014:   Folien 179-189

    Weiter mit Kapitel 3: Logik-Programmierung - heute: Rekursive Programme und Datentypen, Vorfahren und Nachkommen, Wege in gerichteten Graphen, Unterschied zwischen Theorie und Praxis, natürliche Zahlen in Unärdarstellung, Listen, Quicksort als Logikprogramm, Beispiele für Beweisbäume

    Material: Folien, Skript zu Kapitel 3 - Teil 2, Quelltext der Programme bibel6.pl, digraph1.pl, digraph2.pl, unat1.pl, listenfkt.pl.
    Weitere Lektüre: Chapter 2 (Database Programming) und Chapter 3 (Recursive Programming) in [SS]

  3. Mi, 26.11.2014:   Folien 190-197

    Weiter mit Kapitel 3: Logik-Programmierung - heute: Beispiele für Logik-Programme: binäre Suchbäume, aussagenlogische Formeln, Normalformen für aussagenlogische Formeln; denotationelle vs. operationelle Semantik

    Material: Folien, Skript zu Kapitel 3 - Teil 3, Quelltext der Programme seachtree.pl, al.pl, alnormalformen.pl, Übungsblatt 5
    Weitere Lektüre: Chapter 3 (Recursive Programming) und Chapter 5.1 (Semantics) in [SS]

  4. Fr, 28.11.2014:   Folien 198-202

    Weiter mit Kapitel 3: Logik-Programmierung - heute: mehr über Substitutionen, Umbenennungen, ein einfacher Interpreter für Logikprogramme, Satz über die Korrektheit und Vollständigkeit des Interpreters, Beweis der Vollständigkeit, d.h. der Richtung (a)=>(b)

    Material: Folien, Skript zu Kapitel 3 - Teil 4
    Weitere Lektüre: Chapter 1.8 und Chapter 5.1 und 5.2 in [SS]

  5. Mi, 03.12.2014:   Folien 200-211

    Weiter mit Kapitel 3: Logik-Programmierung - heute: Beweis der Korrektheit, d.h. der Richtung (b)=>(a) des Interpreters ANTWORT(Pi,alpha); Unifikation, allgemeinste Unifikatoren (kurz: mgu, für "most general unifier"), Lemma zur Eindeutigkeit von mgus (ohne Beweis) ein Algorithmus zum Finden allgemeinster Unifikatoren; ein Interpreter für Logikprogramme mit allgemeinsten Unifikatoren (der Algorithmus UANTWORT(Pi,alpha)), Satz über die Korrektheit und Vollständikeit des Algorithmus UANTWORT (ohne Beweis); abschließende Bemerkungen zur Implementation des Interpreters in logischen Programmiersprachen

    Material: Folien, Skript zu Kapitel 3 - Teil 5, Übungsblatt 6
    Weitere Lektüre: Chapter 4 in [SS]

  6. Fr, 05.12.2014:   Folien 212-245

    Abschluss von Kapitel 3: Logik-Programmierung - heute: Prolog: ein Prologinterpreter (der Algorithmus PANTWORT(Pi,alpha)), Vergleich zwischen der deklarativen Semantik und der Prolog-Semantik von Logik-Programmen, Terminierung, Beispiele, Suchbäume, das in Prolog eingebaute Prädikat ! (Cut), Unifikation in Prolog

    Material: Folien, Skript zu Kapitel 3 - Teil 6, Quelltext der Programme bsp1-PAntwort.pl, myplus1.pl, myplus2.pl, myplus3.pl, cutbsp2.pl
    Weitere Lektüre: Chapter 5.4, Chapter 6 und Chapter 7 in [SS]

  7. Mi, 10.12.2014:   Folien 246-265

    Start mit Kapitel 4: Logik erster Stufe - heute: Signaturen, Strukturen, Eigenschaftern 2-stelliger Relationen, Äquivalenzrelationen, Ordnungen, arithmetische Strukturen, Wörter als Strukturen, Transitionssysteme, relationale Datenbanken als Strukturen

    Material: Folien, Skript zu Kapitel 4 - Teil 1, Übungsblatt 7
    Weitere Lektüre: Kapitel I und Kapitel III.1 in [EFT]. Einen Überblick über die Rolle der Logik in der Informatik gibt der Artikel "On the unusual effectiveness of logic in computer science" von Halpern, Harper, Immerman, Kolaitis, Vardi und Vianu (Bulletin of Symbolic Logic 7(2):213-236 (2001)), den Sie hier finden. Einen Überblick über die Geschichte der logischen Grundlagen der Mathematik gibt der Comic Logicomix.

  8. Fr, 12.12.2014:   Folien 266-289

    Weiter mit Kapitel 4: Logik erster Stufe - heute: Strukturen aus Logikprogrammen, Restriktionen und Expansionen, Isomorphie, Variablen, Terme der Logik erster Stufe, Belegungen, Interpretationen, Semantik von Termen, Vergleich zwischen Aussagenlogik und Logik erster Stufe, das Alphabet der Logik erster Stufe

    Material: Folien, Skript zu Kapitel 4 - Teil 2
    Weitere Lektüre: Kapitel III.1 und Kapitel II.1-3 in [EFT].

  9. Mi, 17.12.2014:   Folien 288-307

    Weiter mit Kapitel 4: Logik erster Stufe - heute: Syntax und Semantik der Logik erster Stufe; viele Beispiele; die freien Variablen einer Formel der Logik erster Stufe; die Modellbeziehung

    Material: Folien, Skript zu Kapitel 4 - Teil 3, Übungsblatt 8
    Weitere Lektüre: Kapitel II.1-3 und Kapitel III.2-3 in [EFT]; Chapter 5.1-5.7 in [B] Kapitel 4.A in [KK]; Kapitel 2.1 und 2.2 in [S]

  10. Fr, 19.12.2014:   Folien 307-317

    Weiter mit Kapitel 4: Logik erster Stufe - heute: Subformeln, Subterme, Syntaxbäume; Beweise per Induktion über den Aufbau von Termen und Formeln der Logik erster Stufe; das Isomorphielemma

    Material: Folien, Skript zu Kapitel 4 - Teil 4
    Weitere Lektüre: Kapitel II.3-4 und Kapitel III.5 in [EFT]; Chapter 5.1-5.7 in [B] Kapitel 4.A in [KK]; Kapitel 2.1 und 2.2 in [S]

  11. Mi, 07.01.2015:   Folien 318-332

    Weiter mit Kapitel 4: Logik erster Stufe - heute: kurze Wiederholung der bisherigen Themen, freie Variablen, Koinzidenzlemma, Sätze der Logik erster Stufe, Modellklassen und Definierbarkeit (bzw. Axiomatisierbarkeit) von Klassen von Strukturen, Beispiele für Formeln der Logik erster Stufe in verschiedenen Anwendungsbereichen: lineare Ordnungen, Arithmetik, Worte

    Material: Folien, Skript zu Kapitel 4 - Teil 5, Übungsblatt 9
    Weitere Lektüre: Kapitel II.5 und Kapitel III.4 und III.6 in [EFT]

  12. Fr, 09.01.2015:   Folien 333-348

    Weiter mit Kapitel 4: Logik erster Stufe - heute: Beispiel für Formeln der Logik erster Stufe in verschiedenen Anwendungsbereichen: Transitionssysteme; Logik und Datenbanken: kurze Wiederholung der Repräsentation einer Kinodatenbank als Struktur über einer geeigneten Signatur; Beispiele für in FO formulierte Anfragen an die Datenbank; die von einer Formel in einer Struktur definierte n-stellige Relation; rekursive Beschreibung dieser Relation, die zu einem Algorithmus führt, der das Auswertungsproblem für FO löst

    Material: Folien, Skript zu Kapitel 4 - Teil 6
    Weitere Lektüre: Kapitel 1.1 in [L], Kapitel 4.3 in [FG]

  13. Mi, 14.01.2015:   Folien 349-364

    Weiter mit Kapitel 4: Logik erster Stufe - heute: Äquivalenz von Formeln der Logik erster Stufe; relationale Signaturen; Ehrenfeucht-Fraisse-Spiele: Spielregeln des m-Runden EF-Spiels, Gewinnbedingung, partielle Isomorphismen, Beispiele, Formalisierung des Begriffs "Gewinnstrategie", Formulierung des Satzes von Ehrenfeucht (ohne Beweis), der Begriff der Quantorentiefe einer FO-Formel, Formulierung der einfachen Version des Satzes von Ehrenfeucht (deren Beweis in der nächsten Vorlesung gegeben wird).

    Material: Folien, Skript zu Kapitel 4 - Teil 7, Übungsblatt 10
    Weitere Lektüre: Kapitel 3.2 und 3.3 in [L]

  14. Fr, 16.01.2015:   Folien 364-367

    Weiter mit Kapitel 4: Logik erster Stufe - heute: Beweis der einfachen Version des Satzes von Ehrenfeucht; Erklärung, wie Spoiler durch "Ausspielen einer Formel" eine Gewinnstrategie erhält; Begriff der FO-Definierbarkeit einer Klasse von σ-Strukturen, Korollar über nicht-FO-definierbare Klassen von σ-Strukturen (der Beweis des Korollars wird in der nächsten Vorlesung gegeben)

    Material: Folien, Skript zu Kapitel 4 - Teil 8
    Weitere Lektüre: Kapitel 3.5 in [L]

  15. Mi, 21.01.2015:   Folien 367-375

    Weiter mit Kapitel 4: Logik erster Stufe - heute: Beweis des Korollars über nicht-FO-definierbare Klassen von Strukturen; das EF-Spiel auf 2 endlichen linearen Ordnungen; Nachweis, dass Duplicator eine Gewinnstrategie im m-Runden EF-Spiel auf 2 endlichen linearen Ordnungen der Kardinalität > 2^m besitzt; Folgerung, dass die Klasse aller endlichen linearen Ordnungen gerader Kardinalität nicht FO-definierbar ist; Beweisskizze des Resultats, das besagt, dass weder Graph-Zusammenhang noch Erreichbarkeit FO-definierbar sind.

    Material: Folien, Skript zu Kapitel 4 - Teil 9, Übungsblatt 11
    Weitere Lektüre: Kapitel 3.2 und 3.6 in [L]

  16. Fr, 23.01.2015:   Folien 375-390

    Abschluss von Kapitel 4: Logik erster Stufe - heute: Beweis des Resultats, das besagt, dass Graph-Zusammenhang nicht FO-definierbar ist; Bemerkung zur Methode der logischen Reduktionen; Erfüllbarkeit, Allgemeingültigkeit und die Folgerungsbeziehung für Formeln der Logik erster Stufe; die Formeln "Verum" und "Falsum"; Normalformen für Formeln der Logik erster Stufe: Negationsnormalform und Pränex-Normalform

    Material: Folien, Skript zu Kapitel 4 - Teil 10
    Weitere Lektüre: Kapitel 3.6 in [L], Kapitel 2.2 in [S],

  17. Mi, 28.01.2015:   Folien 391-412

    Start mit Kapitel 5: Grundlagen des automatischen Schließens - heute: Ableitungsregeln, Kalküle, Ableitungen, Beispiele für Kalküle (zur Definition bestimmter Mengen natürlicher Zahlen, zur Definition der syntaktisch korrekten aussagenlogischen Formeln, Resolutionskalkül der Aussagenlogik, Kalkül zur Beschreibung der aus einem Logik-Programm ableitbaren Terme); Mengen, die unter einem Kalkül abgeschlossen sind; Charakterisierung aller aus einer Menge V in einem Kalkül K ableitbaren Elemente als die kleinste unter K abgeschlossene Menge, die jedes Element aus V enthält; Induktionsprinzip für die Menge der ableitbaren Elemente eines Kalküls; Notationen für Logik erster Stufe, der Begriff einer "Sequenz", die Menge MS aller Sequenzen, Korrektheit von Sequenzen; Korrektheit, Vollständigkeit und Effektivität von Kalkülen über der Menge MS

    Material: Folien, Skript zu Kapitel 5 - Teil 1, Übungsblatt 12
    Weitere Lektüre: Kapitel IV.1 in [EFT],

  18. Fr, 30.01.2015:   Folien 412-428

    Weiter mit Kapitel 5: Grundlagen des automatischen Schließens - heute: der Begriff der Korrektheit von Sequenzenregeln; der Sequenzenkalkül kS (bestehend aus Grundregeln, aussagenlogischen Regeln, Quantorenregeln und Gleichheitsregeln); Substitutionen und das Substitutionslemma (ohne Beweis); die Korrektheit des Sequenzenkalküls kS; Beispiele für Ableitungen im Sequenzenkalkül; ein mittels Ableitungen im Sequenzenkalkül kS definierter Begriff der Beweisbarkeit von Formeln aus Formelmengen

    Material: Folien, Skript zu Kapitel 5 - Teil 2
    Weitere Lektüre: Kapitel IV.2-4, IV.6 und III.8 in [EFT], Kapitel 2.2 in [S]

  19. Mi, 04.02.2015:   Folien 428-439

    Weiter mit Kapitel 5: Grundlagen des automatischen Schließens - heute: Widerspruchsfreie und widerspruchsvolle Formelmengen; der Vollständigkeitssatz und das Erfüllbarkeitslemma; der Endlichkeitssatz; erststufige Axiomatisierbarkeit; Beweis der Nicht-Axiomatisierbarkeit der Endlichkeit und der Nicht-Axiomatisierbarkeit von Graph-Zusammenhang

    Material: Folien, Skript zu Kapitel 5 - Teil 3
    Weitere Lektüre: Kapitel IV.7, V und VI.2 in [EFT]

  20. Fr, 06.02.2015:   Folien 441-455

    Weiter mit Kapitel 5: Grundlagen des automatischen Schließens - heute: der Satz von Löwenheim und Skolem (ohne Beweis); die Grenzen der Berechenbarkeit: Entscheidungsprobleme für die Logik erster Stufe, die Semi-Entscheidbarkeit des Allgemeingültigkeitsproblems, des Unerfüllbarkeitsproblems und des Folgerungsproblems für die Logik erster Stufe, Nachweis der Unentscheidbarkeit dieser Probleme (durch Nutzen der Unentscheidbarkeit des Postschen Korrespondenzproblems), Nachweis der Nicht-Semi-Entscheidbarkeit des Erfüllbarkeitsproblems für die Logik erster Stufe

    Material: Folien, Skript zu Kapitel 5 - Teil 4
    Weitere Lektüre: Kapitel 2.3 in [S] und Kapitel VI.1 und X.1-4 in [EFT]

  21. Mi, 11.02.2015:   Folien 456-466

    Abschluss von Kapitel 5: Grundlagen des automatischen Schließens - heute: Der Satz von Herbrand - genauer: Grundterme, Herbrandstrukturen, gleichheitsfreie Formeln, Formeln in Skokemform, Herbrand-Expansionen, der Satz von Gödel-Herbrand-Skolem, der Satz von Herbrand, Anwendung des Satzes, Skolemisierung

    Material: Folien, Skript zu Kapitel 5 - Teil 5
    Weitere Lektüre: Kapitel 2.4 in [S] und Kapitel XI.1 in [EFT]

  22. Fr, 13.02.2015:  

    Hilfestellungen zur Klausurvorbereitung. Inbes.: Details zum Ablauf der Klausur und Durcharbeiten einiger Beispiel-Aufgaben

    Material: Wichtige Hinweise zum Ablauf der Klausur finden Sie hier.
    Ein Muster für das Deckblatt der Klausur finden Sie hier.
    Das Layout der Klausur wird in etwa so aussehen wie das Layout der Beispielklausuren, die am Ende des hier erhältlichen Skripts zur Vorlesung "Diskrete Modellierung" (Goethe-Universität Frankfurt am Main) zu finden sind. Beachten Sie dazu aber, dass die Veranstaltung "Logik in der Informatik" der HU Berlin eine ganz andere Schwerpunktsetzung hat als die "Diskrete Modellierung" der Goethe-Univ. Frankfurt (insbes. hat die Klausur "Diskrete Modellierung" eine Dauer von nur 120 Minuten, die Vorlesung richtet sich an Studierende im 1. Semester und hat nur 3 SWS, und das Thema Logik spielt in der Vorlesung "Diskrete Modellierung" eine untergeordnete Rolle, während es in der "Logik in der Informatik" der HU Berlin das zentrale Thema ist).


Last modified: January 07, 2015
Nicole Schweikardt