 |
| Wir freuen uns über zu diesen Seiten. |
|
| Letzte Änderung:
17.01.2013 |
|
|
|
| 18.001 Vorlesung: Formale Grundlagen der Informatik 1 (F1): Logik |
| Veranstalter |
| Christopher Habel |
| Carola Eschenbach |
| Zeit/Ort |
| Di 10-12 Phil A |
| Inhalt |
| Übergeordnete Lernziele des Zyklus sind: Methoden der (strukturellen) Mathematik für
informatische Probleme anwenden zu können. Definitionsprinzipien und Beweistechniken kennen
zu lernen und diese in unterschiedlichen Bereichen anwenden zu können. Formale Konzepte der
Modellierung kennen zu lernen und zum Einsatz zu bringen. Die Grenzen der prinzipiellen
Möglichkeiten mit Hilfe von theoretisch fundierten Aussagen benennen und einschätzen zu
können. Kennenlernen und Vertrautwerden mit grundlegenden formalen Konzepten und Methoden,
die für fast alle Teilgebiete der Informatik wichtig sind. Erwerben und Einüben der
einfachsten Standardhilfsmittel für Beschreibung, Analyse, Entwurf und Bewertung von
Problemen und deren Lösung.
- Einführung in die Aussagenlogik: wohlgeformte Ausdrücke, Wahrheitswerte,
Wahrheitstafeln, Belegungsfunktion, Grundkonzepte der Semantik: Allgemeingültigkeit,
Unerfüllbarkeit, Erfüllbarkeit und Folgerung
- Beweistheorie und Ableitungssysteme für die Aussagenlogik: Schlussregeln, modus
ponens, Beziehung zwischen Semantik und Beweisverfahren, Vollständigkeit und
Korrektheit von Beweisverfahren
- Mechanisierung des aussagenlogischen Beweisens: Normalformen, Literale und
Klauseln, Resolutionsverfahren, Hornklauseln
- Die Syntax der Prädikatenlogik erster Stufe: Charakterisierung wohlgeformter
Ausdrücke, Quantoren und Quantorenskopus, freie und gebundene Variablen,
geschlossene Formeln
- Semantik der Prädikatenlogik: Modell, Interpretation, Allgemeingültigkeit,
Unerfüllbarkeit, Erfüllbarkeit, Folgerung
- Ableitungssysteme und mechanisches Beweisen in der Prädikatenlogik: Normalformen,
Skolemisierung, Resolutionsverfahren der Prädikatenlogik, Grundresolutionssatz,
Unifikation, allgemeinster Unifikator, P- und N-Stützmengen, Resolutionsverfahren,
Beziehung zwischen Semantik und Ableitungssystemen
|
|
| Literatur |
| Die Vorlesung orientiert sich mit Auswahl des Inhaltes und der Notation an:
- Schöning, Uwe (2000). Logik für Informatiker. Heidelberg: Spektrum. (5.Aufl.)(ca.
18 EUR)
|
Ergänzend zum Kauf und Lesen empfohlen:
- Salmon, Wesley C. (1983). Logik. Reclam (ca. 7 EUR)
|
Für mathematische Ergänzungen:
- Biggs, Norman L. (1989). Discrete Mathematics. Oxford: Clarendon Press
- Reinhardt, Fritz & Heinrich Soeder (1974). dtv-Atlas zur Mathematik. Band
1: Grundlagen, Algebra und Geometrie. München: Deutscher Taschenbuch Verlag (ca. 13 EUR)
|
Weiterführend (auch für das Hauptstudium):
- Davis, Ruth E. (1989). Truth, Deduction, and Computation. New York: W.H. Freeman.
(Computer Science Press.)
- Galton, Antony (1990). Logic for Information Technology.Chichester: Wiley
- Gamut, L. T. F. (1991). Logic, Language, and Meaning. vol 1 & vol 2.
Chicago: The University of Chicago Press
- Manna, Zohar & Waldinger, Richard (1985). The Logical Basis for Computer
Programming. Vol 1: Deductive Reasoning. Reading, MA: Addison Wesley
- Ben-Ari, Mordechai (2001). Mathematical Logic for Computer Science. Springer: London
- Fitting, Melvin (1996). First-Order Logic and Automated Theorem Proving. Springer:
New York
- Nerode, Anil & Richard A. Shore (1997). Logic for Application. Springer:
New York
|
|
| Folien |
|
Das Ausdrucken der Folien über Universitätsdrucker ist nicht zulässig. Folienkopien
werden zu Semesteranfang zur Verfügung gestellt.
gesamter Foliensatz
Korrekturen und Ergänzungen
|
| Links |
|
|
|
