Symbolisches Rechnen

Automatisches Beweisen Vertiefung

Modulinhalt:

  1. Logik erster Stufe (FOL)
  2. Entscheidbare FOL Fragmente: Lineare Arithmetik, Gleichheit und uninterpretierte Funktionen, Quantorenelimination
  3. Modal-Logiken & Temporal-Logiken: Model Checking und Symboic Model Checking