Bilder vom Neuenheimer Feld, Heidelberg und der Universität Heidelberg

Lehrveranstaltungen
HISPOS und LSF
Signup	FAQ
Fachschaft	Ressourcen

HS Deduktionssysteme

Kurt Eberle
Email: k.eberle@lingenio.de
Do 18.15-19.45, KStr. 2, R 004
(11 Sitzungen, eventuell eine zusätzliche Sitzung 1 Klausur)

Ziel:

Ziel dieses Kurses ist es einen Überblick über verschiedene Beweisverfahren zu geben.Ausgehend von der Prädikatenlogik der ersten Stufe werden verschiedene Kalküle des Schließens, insbesondere Gentzenkalküle und Resolution vorgestellt. Es werden verschiedene Repräsentationsvarianten solcher Kalküle, wie Tableaukalkül und Matrizen,diskutiert, sowie zugehörige Kontrollmechanismen. Weitere Themen sind: Gleichungslogik, Paramodulation, Termersetzung, Unifikation. Falls die Zeit es erlaubt, werden Beweisverfahren für Logiken höherer
Stufe und Modal- bzw. Temporallogiken skizziert.

Leistungsnachweis:

Das Hauptseminar ist nur erfolgreich absolviert, wenn mindestens die Hälfte der Hausaufgaben rechtzeitig, d.h.bis zum jeweils nächsten Seminartermin, erledigt wurden und wenn die Klausur am Ende des Semesters mit ausreichendem Erfolg geschrieben wurde. Die Note ist die Note der Klausur.

Unterlagen:

Literatur.

Übersicht:

Materialien: (Datum anklicken)		Aufgaben	Lösungen
29.04.	Vorbesprechung, Einführung, Geschichte des automatischen Beweisens
6.05.	Prädikatenlogik, Syntax und Semantik	Aufgabe 1
13.05.	Termmodell, Herbrand-Modell, Normalformen	Aufgabe 2
27.05.	Skolemisierung, sortierte Logik, Modellbildung	Aufgabe 3	Lösungen
3.06.	Resolutionsregel, Unifikation Korrektheit der Resolution in Aussagen- und Prädikatenlogik	Aufgabe 4	Lösungen
17.6.	Substitution, Unifikation, allgemeinster Unifikator Resolution: korrekter und vollständiger Testkalkül partielle und totale Theorieresolution	Aufgabe 5	Lösungen
24.06.	Deduktive Kalküle, Testkalküle, Gentzenkalkül	Aufgabe 6	Lösungen
1.07.	Repräsentationen, Tableaukalkül, Tilgungsregeln, Klauselgraphen	Aufgabe 7
8.07.	Restriktions- und Ordnungsstrategien: Gängige Resolutionsverfahren	Aufgabe 8
15.7.	Resolutionsverfahren, Matrizen, Gleichheitsverfahren
21.07.	Gleichheitsverfahren: Paramodulation, Unifikation, Termersetzung Ausblick: Jenseits von PL1
22.07.	Klausur	Klausur
29.07.	Ersatztermin: Nachzügler-Klausur