Knowledge about unification theory and its applications.
In many symbol-oriented systems like expert systems, automated theorem provers, and logic-oriented programming languages (e.g. Prolog) the basic data structures are terms, and the basic operation on terms is unification. Unification tries to make terms equal by replacing variables; algebraically unification can be viewed as the process of solving term equations. Particular topics: Unification in the free term algebra, efficient algorithms; unification in equational theories, results about particular theories like A, C, AC, AC1, Boolean rings; universal unification; combination of unification procedures; applications of unification in automated theorem proving, term rewriting, logic programming, linguistics etc.
First meeting: Wednesday, 11 March 2015, 15:00, seminar room "Gödel" (Favoritenstr. 9/ground floor/courtyard). Please register for the course via TISS, or if this fails, via email to salzer@logic.at. If necessary the course will be given in English.
20 h attendance of lecture (10 days x 2h)25 h exercises (25 x 1h)14 h preparation of presentation14 h preparation for final test 2 h final test-----------------------------------------75 h = 3 Ects
