Lehrveranstaltungsleiter: Alexander Leitsch
Diese Lehrveranstaltung ist Wahlfach im Magisterstudium Computational Intelligence.
First Meeting:
Monday, October 5 2009, 13:15
Zemanek-Hörsaal,
Favoritenstrasse 9, ground floor
CONTENT: Higher-order unification
It is well known that, in contrast to first-order unification, the unification problem becomes undecidable already in second-order logic. However there are interesting subclasses of simple type theory where unification is decidable (ramified type theory). The subject of this seminar is a detailed analysis of a paper on unification in ramified type theory where this result has been shown. Moreover applications to theorem proving in the weak second-order arithmetic ACA_0 are discussed. As a preparation the general unification method for type theory (as invented by G. Huet) will be presented.
Time and Place: Tuesday 11-13, Labor Room 185/2, Favoritenstraße 9, 3rd floor, yellow zone (beginning October 13).
Material:
Jean Goubault-Larrecq: Ramified higher-order unification, Wayne Snyder and Jean H. Gallier: higher order unification revisited: complete sets of transformations.
Requirements: firm background in logic and Lambda-calculus, basic knowledge in type theory is desirable.
A.Leitsch