Fixpunkte

   - Elimination von prozeduraler Rekursion in SML
   - Fixpunktsatz 

IMP

   - operationale Semantik
   - denotationale Semantik

Hoare-Logik

   - partielle und totale Korrektheit
   - Hoare-Regeln
   - Schleifeninvarianten und Verfikationsbedigungen
   - Verifikation mit der VC-Methode
   - schwächste Vorbedingungen

Aussagenlogik

   - Substitution A[B/X] und Ersetzungssatz
   - disjunktive und konjunktive Vereinfachung
   - geschlossene Tableaus
   - Res(S) und Ber(S)
   - Resolutionssätze
   - Berechnung von Primdarstellungen
   - Primdarstellungssatz
   - Kompaktheitssatz

ASSN und Prädikatenlogik

   - Bindungsstruktur, freie Variablen
   - Substitutionsfunktion (ASSN)
   - Formalisierung in ASSN
   - Transfersätze 10.3.3 und 10.4.2
   - Vereinfachungssatz 10.6.5
   - Berechnung von quantorenfreien Klauseldarstellungen
   - Expansionssatz 10.7.7
   - Unifikationssatz 
   - Berechnung prinzipaler Unifikatoren
   - Resolutionabschlüsse Res(S) und Res(r,S)
   - Resolutionsgraphen

Berechenbarkeit

   - Testbarkeit und Entscheidbarkeit
   - Gödels Unvollständigkeitssatz
   - Berechenbarkeitseigenschaften von Hoare- und
     Prädikatenlogik