Grundlagen der Logik für Informatiker (GLoIn)5 ECTS
(englische Bezeichnung: Logic for Computer Scientists)
(Prüfungsordnungsmodul: Grundlagen der Logik in der Informatik)

Lehrveranstaltungen:

• • Grundlagen der Logik in der Informatik
    (Vorlesung, 2 SWS, Lutz Schröder, Do, 8:30 - 10:00, HH, (außer Do 27.11.2014, Do 29.1.2015); Einzeltermine am 27.11.2014, 29.1.2015, 8:30 - 10:00, HG)
  • Übungen zu Grundlagen der Logik in der Informatik
    (Übung, 2 SWS, Sergey Goncharov)
  • Intensivübung zu Grundlagen der Logik in der Informatik (optional)
    (Übung, 2 SWS, Sergey Goncharov)

Inhalt:

Aussagenlogik:

• Syntax und Semantik

• Automatisches Schließen: Resolution

• Formale Deduktion: Korrektheit, Vollständigkeit

Prädikatenlogik erster Stufe:

• Syntax und Semantik

• Automatisches Schließen: Unifikation, Resolution

• Quantorenelimination

• Anwendung automatischer Beweiser

• Formale Deduktion: Korrektheit, Vollständigkeit
  

Lernziele und Kompetenzen:

• Erwerb fundierter Kenntnisse zu den Grundlagen und der praktischen Relevanz der Logik mit besonderer Berücksichtigung der Informatik;

• Verstehen und Erklären des logischen Schließens;

• Einübung in das logische und wissenschaftliche Argumentieren, Aufstellen von Behauptungen und Begründungen;

• Kritische Reflexion von Logikkalkülen, insbesondere hinsichtlich Entscheidbarkeit, Komplexität, Korrektheit und Vollständigkeit;

• Erstellung und Beurteilung von Problemspezikationen (Kohärenz, Widerspruchsfreiheit) und ihre Umsetzung in Logikprogramme;

• Beherrschung der praktischen Aspekte der Logikprogrammierung.

Fachkompetenz

Wissen

Die Studierenden
– geben Definitionen zur Syntax und Semantik der verwendeten Logiken wieder
– beschreiben grundlegende Deduktionsalgorithmen
– geben Regeln der verwendeten formalen Deduktionssysteme wieder

Verstehen

Die Studierenden
– erläutern das Verhältnis zwischen Syntax, Semantik und Beweistheorie der verwendeten Logiken
– erklären die Funktionsprinzipien grundlegender Deduktionsalgorithmen
– erläutern die Funktionsweise automatischer Beweiser
– erläutern grundlegende Resultate der Metatheorie der verwendeten Logiken und deren Bedeutung

Anwenden

Die Studierenden
– wenden Deduktionsalgorithmen auf konkrete Deduktionsprobleme an
– formalisieren Anwendungsprobleme in logischer Form und verwenden automatische Beweiser zur Erledigung entstehender Beweisziele
– führen einfache formale Beweise manuell

Analysieren

Die Studierenden führen einfache metatheoretische Beweise, inbesondere durch syntaktische Induktion

Lern- bzw. Methodenkompetenz

Die Studierenden beherrschen das grundsätzliche Konzept des Beweises als hauptsächliche Methode des Erkenntnisgewinns in der theoretischen Informatik. Sie überblicken abstrakte Begriffsarchitekturen.

Sozialkompetenz

Die Studierenden lösen abstrakte Probleme in Gruppenarbeit.

Literatur:

Schöning, U.: Logik für Informatiker. Heidelberg: Spektrum Akademischer Verlag, 2000

Barwise, J., and Etchemendy, J.: Language, Proof and Logic; CSLI, 2000.

Huth, M., and Ryan, M.: Logic in Computer Science; Cambridge University Press, 2000.

Weitere Informationen:

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:

1. Wirtschaftsinformatik (Bachelor of Science)
   (Po-Vers. 2010 | Pflichtbereich (Methodenkompetenz) | weitere Pflichtmodule | Informatik | Grundlagen der Logik in der Informatik)

Studien-/Prüfungsleistungen:

Grundlagen der Logik für Informatiker (Prüfungsnummer: 30711)

Prüfungsleistung, Klausur, Dauer (in Minuten): 90, benotet

Anteil an der Berechnung der Modulnote: 100.0 %

weitere Erläuterungen:
Die im Rahmen der Übungen gestellten Übungsaufgaben können abgegeben werden und werden in diesem Fall bewertet. Auf Basis des Ergebnisses dieser Bewertungen können bis zu 15% Bonuspunkte erworben werden, die zu dem Ergebnis einer bestandenen Klausur hinzugerechnet werden.

Erstablegung: WS 2014/2015, 1. Wdh.: SS 2015

1. Prüfer:

Lutz Schröder

Termin: 24.03.2015, 13:00 Uhr, Ort: s. Aushang
Termin: 21.09.2015, 11:00 Uhr, Ort: H 14
Termin: 22.03.2016, 11:00 Uhr, Ort: s. Aushang
Termin: 23.09.2016, 16:00 Uhr, Ort: H 8 TechF