Formale Logik findet sich in vielen Teilen der Informatik. Logikgatter
Bausteine sind die Grundbausteine integrierter Schaltkreise. Beweise
der NP-Vollständigkeit basieren oft auf Reduktion auf Probleme der
Erfüllbarkeit aussagenlogischer Formeln (3SAT).
Formale Logik bietet Definitionen des Konzepts "Berechenbarkeit" und
ist eine reiche Quelle für Probleme, die nicht algorithmisch gelöst werden
können. Aussagenlogik, Prädikatenlogik und temporale Logik werden zur
Verifikation der Korrektheit von Algorithmen oder Programmen genutzt.
Diese Vorlesung bietet eine Einführung in formale Logik. Die Grundlagen
(Formel, Erfüllbarkeit, Belegung, ...) werden anhand der Aussagenlogik
erläutert. Dann widmen wir uns zentralen Konzepten der Prädikatenlogik,
bis hin zur Vollständigkeit und den
Gödelschen Sätzen, sowie der modalen Logik (temporale Logik).
Übungen:
Hier werden die Übungsblätter bereit gestellt.
Abgabe diesmal nur einzeln! Sie dürfen gerne zusammenarbeiten, es ist
aber wichtig, dass sich jeder mit allen Aufgaben befasst, sonst
lernt man nicht genug für die Klausur.
Wer in den Tutorien zwei (korrekte) Lösungen präsentiert,
bekommt in der Klausur einen Bonuspunkt.