Theoretische Informatik und Logik(SS2016): Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Tobias Philipp (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
Tobias Philipp (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 62: | Zeile 62: | ||
* 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 | * 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 | * 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]), 5. Übungswoche | * 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]), 5. Übungswoche | * 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]), 5. Übungswoche | * 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]), 5. Übungswoche | * Unifikationsprobleme II ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_B_anwendung2_task_A.pdf Aufgabenstellung]), 5. Übungswoche | ||
<br> | <br> | ||
* 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 | * 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 | * 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 === | ||
| Zeile 83: | Zeile 78: | ||
* Schrittweiser Resolutionsbeweis ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.6_B_Res1ordKlausurBeweis_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]), 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]), 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]), 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]), 7. Übungswoche | * 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 | ||
Version vom 24. Mai 2016, 20:06 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
Neuigkeiten
- Für die nächsten zwei Übungsblätter habt Ihr die Möglichkeit Eure Lösungen bis zum Montag den 23.5. und Montag den 30.5. bis um 14 Uhr abzugeben (in den Briefkasten zwischen der 2005 und 2006 in APB).
Vorlesung
Die Vorlesung findet montags in der 2. DS in APB/E023 und donnerstags in der 4. DS in HSZ/0004 statt.
Am Montag, den 30.05.2016, findet die Vorlesung ausnahmsweise in CHE (Chemie-Hörsaal) 91 statt.
Vorlesungsfolien
- Einführung
- Prädikatenlogik erster Stufe (aktualisiert am 9.5.2015, 9:45 Uhr)
- Folien Theoretische Informatik
Übungen
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 Freitag, 14 Uhr (in der Woche vor der entsprechenden Übungswoche) in den Briefkasten zwischen der 2005 und 2006 (in APB) einwerfen.
- Dienstag, 5.DS in APB/E010
- Mittwoch, 4.DS in APB/E010
- Mittwoch, 5.DS in APB/E001
- Freitag, 2.DS in APB/E008
- Freitag, 5.DS in APB/E007
Aufgaben zur Prädikatenlogik
Lösungen zu fast allen Übungsaufgaben, und weitere Übungsufgaben finden sich in dem Buch "S. Hölldobler et al.: Logik und Logikprogrammierung, Band II: Aufgaben und Lösungen, Synchron Publishers GmbH, 2011""
4.1 Syntax
- Konstruktion von Teiltermen (Aufgabenstellung), 1. Übungswoche
- Über Nachbarn (Aufgabenstellung), 1. Übungswoche
4.2 Substitutionen
- Substitutionskomposition ist eine Substitution (Aufgabenstellung), 2. Übungswoche
- Eigenschaften von Substitutionen (Aufgabenstellung), 2. Übungswoche
4.3 Semantik
- Beispiele zur Interpretationsanwendung (Aufgabenstellung), 3. Übungswoche
- Verschiedene Interpretationen einer Formel (Aufgabenstellung), 3. Übungswoche
- Existenz einer Herbrand-Interpretation (Aufgabenstellung), 3. Übungswoche
- Knifflige Existenz (Aufgabenstellung), 4. Übungswoche
- Falscher Satz für einelementige Domänen (Aufgabenstellung), 4. Übungswoche
- Formel ohne endliche Modelle (Aufgabenstellung), 4. Übungswoche
4.4 Äquivalenz und Normalform
- Modellverlust beim Skolemisieren (Aufgabenstellung), 5. Übungswoche
- Normalformen (Aufgabenstellung), 5. Übungswoche
4.5 Unifikation
- Unifikationsprobleme I (Aufgabenstellung), 5. Übungswoche
- Unifikationsprobleme II (Aufgabenstellung), 5. Übungswoche
- Vergleichbarkeit von Unifikatoren (Aufgabenstellung), 6. Übungswoche
- Zur Terminierung des Unifikationsalgorithmus (Aufgabenstellung), 6. Übungswoche
4.6 Beweisverfahren
- Resolutionsverfahren (Aufgabenstellung), 7.Übungswoche
- Schrittweiser Resolutionsbeweis (Aufgabenstellung), 7.Übungswoche
- Notwendigkeit der Faktorisierung (Aufgabenstellung), 7. Übungswoche
4.7 Implementierung von Beweisverfahren
4.8 Eigenschaften
- Beispiel für korrespondierendes Herbrand-Modell (Aufgabenstellung), 7. Übungswoche
Klausur
Alte Klausuren über Prädikatenlogik sind hier zu finden: [1]
