Theoretische Informatik und Logik(SS2016): Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Emma Dietz (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
Tobias Philipp (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 35: | Zeile 35: | ||
* [https://ddll.inf.tu-dresden.de/w/images/0/0e/Fol2016.pdf Prädikatenlogik erster Stufe] | * [https://ddll.inf.tu-dresden.de/w/images/0/0e/Fol2016.pdf Prädikatenlogik erster Stufe] | ||
* [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] | ||
== Übungen 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 ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.1_A_TeiltermeBachelors_task_A.pdf Aufgabenstellung]), 1. Übungswoche | |||
* Über Nachbarn ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.1_B_Nachbarn_task_A.pdf Aufgabenstellung]), 1. Übungswoche | |||
<!-- | |||
=== 4.2 Substitutionen === | |||
* Substitutionskomposition ist eine Substitution ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.2_A_KomposIsSubst_task_A.pdf Aufgabenstellung]) | |||
* Eigenschaften von Substitutionen ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.2_B_eigenschaften_task_A.pdf Aufgabenstellung]) | |||
=== 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]) | |||
* Verschiedene Interpretationen einer Formel ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_B_IntBeispiele_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]) | |||
* Knifflige Existenz ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.3_D_KniffligEX_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]) | |||
* 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.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]) | |||
* Normalformen ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.4_B_normalformen_task_A.pdf Aufgabenstellung]) | |||
=== 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 II ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_B_anwendung2_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]) | |||
* Zur Terminierung des Unifikationsalgorithmus ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.5_D_UnifTermin_task_A.pdf Aufgabenstellung]) | |||
=== 4.6 Beweisverfahren === | |||
* Resolutionsverfahren ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.6_A_Res1ordBeisp_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]) | |||
* Notwendigkeit der Faktorisierung ([http://www.wv.inf.tu-dresden.de/Teaching/SS-2013/logik/uebungen/4.6_C_Res1ordFactoris_task_A.pdf Aufgabenstellung]) | |||
=== 4.7 Implementierung von Beweisverfahren === | |||
=== 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]) | |||
--> | |||
== Klausur == | |||
Alte Klausuren über Prädikatenlogik sind hier zu finden: [http://www.wv.inf.tu-dresden.de/Teaching/Logik/Klausuren/index.html] | |||
}} | }} | ||
Version vom 6. April 2016, 15:51 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
Die Slots der ursprünglichen Übungsstunden und die Räume wurden verändert. Falls Ihr Euch schon in eine Übung eingeschrieben habt, überprüft bitte ob diese mit den neuen Uhrzeiten übereinstimmt.
Übungen
Die Übungen finden erst ab der zweiten Vorlesungswoche statt, d.h. ab der Woche vom 11.4. Voraussichtlich werden folgende Übungen stattfinden:
- 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
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
Übungen 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
Klausur
Alte Klausuren über Prädikatenlogik sind hier zu finden: [1]
