Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage neue Methoden der Automatischen Deduktion und der Beweistheorie zu erlernen und zu gebrauchen. Insbesondere werden die Studierenden neue Kenntnisse in der induktiven Inferenz erwerben.
Induktive Strukturen und Schemata. Automatische Analyse induktiver Beweise, schematische Schnittelimination, Widerlegung von Formelschemata. Schematische CERES-Methode, Herbrand Systeme, schematische Unifikation.
Die in diser Lehrveranstaltung verwendeten Methoden sind deduktiver Natur. Insbesondere handelt es sich um die Anwendung von Methoden aus der Mathematischen Logik auf die Automatische Deduktion.
Der Leistungsnachweis erfolgt durch die Abhaltung zweier Vorträge im Seminar und durch die Mitarbeit.
Nicht erforderlich
Gute Kenntnisse in Mathematischer Logik, Basiskenntnisse in der Automatischen Deduktion
