Vermittlung von Wissen über Unifikationstheorie und ihre Anwendungen.
In vielen symbolorientierten Systemen wie Expertensystemen, automatischen Beweisern und logikorientierten Programmiersprachen (z.B. Prolog) stellen Terme die grundlegende Datenstruktur dar, wobei die Unifikation als Basisoperation auf Termen dient. Unifikation versucht Terme gleichzumachen, indem Variablen durch geeignete Werte ersetzt werden. Algebraisch gesehen entspricht Unifikation dem Lösen von Termgleichungen. Spezielle Themen: Unifikation in der freien Termalgebra, effiziente Algorithmen; Unifikation in Gleichheitstheorien, Resultate über spezielle Theorien wie A, C, AC, AC1, boolsche Ringe; universelle Unifikation; Kombination von Unifikationsprozeduren; Anwendungen der Unifikationstheorie im automatischen Beweisen, in Termersetzungssystemen, in der logikorientierten Programmierung, in der Linguistik usw.
Erstes Treffen: Mittwoch, 11.März 2015, 15:00, Seminarraum "Gödel" (Favoritenstr. 9/Erdgeschoß/Zugang vom Innenhof) Bitte melden Sie sich zur Lehrveranstaltung über TISS an, oder wenn das nicht geht, per Email an salzer@logic.at. Bei Bedarf wird die Lehrveranstaltung auf Englisch gehalten.
20 h Vorlesungsbesuch (10 Tage x 2h)25 h Übungsbeispiele (25 x 1h)14 h Vorbereitung des Vortrags14 h Vorbereitung auf Abschlusstest 2 h Abschlusstest------------------------------------75 h = 3 Ects
