Theoretische Informatik und Logik(SS2016): Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Tobias Philipp (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
Maximilian Marx (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| (53 dazwischenliegende Versionen von 4 Benutzern werden nicht angezeigt) | |||
| Zeile 6: | Zeile 6: | ||
|Term=SS | |Term=SS | ||
|Year=2016 | |Year=2016 | ||
|Lecture series=Theoretische Informatik und Logik | |||
|Module=INF-B-290 | |Module=INF-B-290 | ||
|SWSLecture=4 | |SWSLecture=4 | ||
| Zeile 11: | Zeile 12: | ||
|SWSPractical=0 | |SWSPractical=0 | ||
|Exam type=Klausur | |Exam type=Klausur | ||
|Description== Neuigkeiten = | |Description=<!-- | ||
= Neuigkeiten = | |||
<b><font color="red">Die Einsichtnahme in die Theoretische Informatik und Logik Klausur vom 25.07.2016 findet am Montag 17.10.2016 um 15:00 Uhr, im Raum 2026 im APB (Andreas-Pfitzmann-Bau / Fakultät Informatik) statt. Ein amtlicher Lichtbildausweis ist mitzubringen.</font> </b> | |||
<b>Es werden keine vorläufigen Klausurergebnisse veröffentlicht.</b> | |||
Der Prüfungstermin ist Montag, der 25.07.2016 um 14:50 Uhr in TRE/PHYS/E. Bitte bereits 10 Minuten vor Beginn (14:40 Uhr) anwesend sein. | |||
* Für die Prüfung gelten folgende Regeln: | |||
** Es sind keine Unterlagen und Hilfsmittel zugelassen. | |||
** Aufgrund des technischen Fortschritts sind auch keine Uhren (wie Telefone) am Platz erlaubt. | |||
* Raumzuordnung (nach Nachname bzw. Studiengang) | |||
** Nachname (beginnt mit) A bis einschließlich SCH: HSZ AUDIMAX | |||
** Alle anderen: HSZ 0003/H | |||
** Studiengang Mathematik unabhängig vom Nachname(!): HSZ 0003/H | |||
** Alle müssen ordnungsgemäß für die Klausur angemeldet sein. | |||
** Bitte bereits 10 Minuten vor Beginn (d.h. 14:40 Uhr) anwesend sein. | |||
| Zeile 20: | Zeile 36: | ||
Die Vorlesung findet montags in der 2. DS in APB/E023 und donnerstags in der 4. DS in HSZ/0004 statt. | Die Vorlesung findet montags in der 2. DS in APB/E023 und donnerstags in der 4. DS in HSZ/0004 statt. | ||
==Vorlesungsfolien== | ==Vorlesungsfolien== | ||
* [https:// | * [https://iccl.inf.tu-dresden.de/w/images/e/e6/Intro2016.pdf Einführung] | ||
* [https:// | * [https://iccl.inf.tu-dresden.de/w/images/0/0e/Fol2016.pdf Prädikatenlogik erster Stufe] (aktualisiert am 9.5.2015, 9:45 Uhr) | ||
* [https://cloudstore.zih.tu-dresden.de/public.php?service=files&t=7d95fbbfa68525629c03913726159ad2 Folien Theoretische Informatik] | * [https://cloudstore.zih.tu-dresden.de/public.php?service=files&t=7d95fbbfa68525629c03913726159ad2 Folien Theoretische Informatik] | ||
* [https://iccl.inf.tu-dresden.de/w/images/6/69/HPaufMPKP.pdf Folien zum Beweis Lemma 6.4] | |||
=Übungen= | =Übungen= | ||
| Zeile 33: | Zeile 48: | ||
Die Übungen finden erst ab der zweiten Vorlesungswoche statt, d.h. ab der Woche vom 11.4. | Die Übungen finden erst ab der zweiten Vorlesungswoche statt, d.h. ab der Woche vom 11.4. | ||
Vor jeder Übung habt die Möglichkeit Eure eigenen Lösungen zu den Aufgaben korrigieren zu lassen. Dafür solltet Ihr diese bis spätestens | Vor jeder Übung habt die Möglichkeit Eure eigenen Lösungen zu den Aufgaben korrigieren zu lassen. Dafür solltet Ihr diese bis spätestens Montag, 15 Uhr (in der Woche der entsprechenden Übungswoche) in den Briefkasten zwischen der 2005 und 2006 (in APB) einwerfen. | ||
* Dienstag, 5.DS in APB/E010 | * Dienstag, 5.DS in APB/E010 | ||
| Zeile 43: | Zeile 58: | ||
== Aufgaben zur Prädikatenlogik == | == Aufgaben zur Prädikatenlogik == | ||
Lösungen zu fast allen Übungsaufgaben, und weitere | Lösungen zu fast allen Übungsaufgaben, und weitere Übungsaufgaben finden sich in dem Buch | ||
"S. Hölldobler et al.: Logik und Logikprogrammierung, Band II: Aufgaben und Lösungen, Synchron Publishers GmbH, 2011"" | "S. Hölldobler et al.: Logik und Logikprogrammierung, Band II: Aufgaben und Lösungen, Synchron Publishers GmbH, 2011"" | ||
| Zeile 54: | Zeile 69: | ||
* Eigenschaften von Substitutionen ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.2_B_eigenschaften_task_A.pdf Aufgabenstellung]), 2. Übungswoche | * Eigenschaften von Substitutionen ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.2_B_eigenschaften_task_A.pdf Aufgabenstellung]), 2. Übungswoche | ||
=== 4.3 Semantik === | === 4.3 Semantik === | ||
* Beispiele zur Interpretationsanwendung ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_A_IntAuswertung_task_A.pdf Aufgabenstellung]) | * Beispiele zur Interpretationsanwendung ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_A_IntAuswertung_task_A.pdf Aufgabenstellung]), 3. Übungswoche | ||
* Verschiedene Interpretationen einer Formel ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_B_IntBeispiele_task_A.pdf Aufgabenstellung]) | * Verschiedene Interpretationen einer Formel ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_B_IntBeispiele_task_A.pdf Aufgabenstellung]), 3. Übungswoche | ||
* Existenz einer Herbrand-Interpretation ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_C_hiexist_task_A.pdf Aufgabenstellung]) | * Existenz einer Herbrand-Interpretation ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_C_hiexist_task_A.pdf Aufgabenstellung]), 3. Übungswoche | ||
* Knifflige Existenz ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_D_KniffligEX_task_A.pdf Aufgabenstellung]) | <br/> | ||
* Falscher Satz für einelementige Domänen ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_E_a468_task_A.pdf Aufgabenstellung]) | * Knifflige Existenz ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_D_KniffligEX_task_A.pdf Aufgabenstellung]), 4. Übungswoche | ||
* Formel ohne endliche Modelle ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_F_a415_task_A.pdf Aufgabenstellung]) | * Falscher Satz für einelementige Domänen ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_E_a468_task_A.pdf Aufgabenstellung]), 4. Übungswoche | ||
* Formel ohne endliche Modelle ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_F_a415_task_A.pdf Aufgabenstellung]), 4. Übungswoche | |||
=== 4.4 Äquivalenz und Normalform === | === 4.4 Äquivalenz und Normalform === | ||
* Modellverlust beim Skolemisieren ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.4_A_modellverlust_task_A.pdf Aufgabenstellung]) | * Modellverlust beim Skolemisieren ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.4_A_modellverlust_task_A.pdf Aufgabenstellung]), 5. Übungswoche | ||
* Normalformen ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.4_B_normalformen_task_A.pdf Aufgabenstellung]) | * Normalformen ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.4_B_normalformen_task_A.pdf Aufgabenstellung]), 5. Übungswoche | ||
=== 4.5 Unifikation === | === 4.5 Unifikation === | ||
* Unifikationsprobleme I ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_A_anwendung_task_A.pdf Aufgabenstellung]) | * Unifikationsprobleme I ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_A_anwendung_task_A.pdf Aufgabenstellung]), 5. Übungswoche | ||
* Unifikationsprobleme II ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_B_anwendung2_task_A.pdf Aufgabenstellung]) | * Unifikationsprobleme II ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_B_anwendung2_task_A.pdf Aufgabenstellung]), 5. Übungswoche | ||
* Vergleichbarkeit von Unifikatoren ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_C_vergleichbarkeit_task_A.pdf Aufgabenstellung]) | <br> | ||
* Zur Terminierung des Unifikationsalgorithmus ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_D_UnifTermin_task_A.pdf Aufgabenstellung]) | * Vergleichbarkeit von Unifikatoren ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_C_vergleichbarkeit_task_A.pdf Aufgabenstellung]), 6. Übungswoche | ||
* Zur Terminierung des Unifikationsalgorithmus ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_D_UnifTermin_task_A.pdf Aufgabenstellung]), 6. Übungswoche | |||
=== 4.6 Beweisverfahren === | === 4.6 Beweisverfahren === | ||
* Resolutionsverfahren ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.6_A_Res1ordBeisp_task_A.pdf Aufgabenstellung]) | * Resolutionsverfahren ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.6_A_Res1ordBeisp_task_A.pdf Aufgabenstellung]), 7. Übungswoche | ||
* Schrittweiser Resolutionsbeweis ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.6_B_Res1ordKlausurBeweis_task_A.pdf Aufgabenstellung]) | * Schrittweiser Resolutionsbeweis ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.6_B_Res1ordKlausurBeweis_task_A.pdf Aufgabenstellung]), 7. Übungswoche | ||
* Notwendigkeit der Faktorisierung ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.6_C_Res1ordFactoris_task_A.pdf Aufgabenstellung]) | * Notwendigkeit der Faktorisierung ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.6_C_Res1ordFactoris_task_A.pdf Aufgabenstellung]), 7. Übungswoche | ||
=== 4.7 Implementierung von Beweisverfahren === | === 4.7 Implementierung von Beweisverfahren === | ||
=== 4.8 Eigenschaften === | === 4.8 Eigenschaften === | ||
* Beispiel für korrespondierendes Herbrand-Modell ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.8_A_korrHbeisp_task_A.pdf Aufgabenstellung]) | * Beispiel für korrespondierendes Herbrand-Modell ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.8_A_korrHbeisp_task_A.pdf Aufgabenstellung]), 7. Übungswoche | ||
== Aufgaben zur Theoretischen Informatik == | |||
=== I. Berechenbarkeit === | |||
* 1. Turingmaschinen ([https://iccl.inf.tu-dresden.de/w/images/b/bc/Uebung8.pdf Aufgabenstellung]), 8. Übungswoche (aktualisiert am 15.6.2016) | |||
* 2. Rekursive Funktionen ([https://iccl.inf.tu-dresden.de/w/images/d/dc/Uebung9.pdf Aufgabenstellung]), 9. Übungswoche | |||
-- | * 3. LOOP- und WHILE-Programme ([https://iccl.inf.tu-dresden.de/w/images/e/e4/Uebung10.pdf Aufgabenstellung]) 10. Übungswoche (aktualisiert am 22.6.2016) | ||
* 4. Post'sches Korrespondenzproblem ([https://iccl.inf.tu-dresden.de/w/images/b/ba/Uebung11.pdf Aufgabenstellung]) 11. Übungswoche | |||
=== II. Komplexität === | |||
* 5. Komplexitätsklasse NP ([https://iccl.inf.tu-dresden.de/web/Datei:ThILUebung12.pdf Aufgabenstellung]) 12. Übungswoche | |||
* 6. Komplexitätsklasse PSpace ([https://iccl.inf.tu-dresden.de/web/Datei:Uebung13.pdf Aufgabenstellung]) 13. Übungswoche | |||
== Klausur == | == Klausur == | ||
Alte Klausuren über Prädikatenlogik sind hier zu finden: [http://www.wv.inf.tu-dresden.de/Teaching/Logik/Klausuren/index.html] | Alte Klausuren über Prädikatenlogik sind hier zu finden: [http://www.wv.inf.tu-dresden.de/Teaching/Logik/Klausuren/index.html] | ||
--> | |||
}} | }} | ||
Aktuelle Version vom 26. Oktober 2020, 18:57 Uhr
Theoretische Informatik und Logik
Lehrveranstaltung mit SWS 4/2/0 (Vorlesung/Übung/Praktikum) in SS 2016
Dozent
- Steffen Hölldobler
Tutor
Umfang (SWS)
- 4/2/0
Module
Leistungskontrolle
- Klausur
Vorlesungsreihe
