Vortrag von Chad Brow (Tschechische Technische Universit?t in Prag): Formalisierung der Mathematik in der Mengenlehre h?herer Ordnung (Mi, 16. November, 14:15-15:45)

Titel: Formalisierung der Mathematik in der Mengenlehre h?herer Ordnung

Referent: Chad Brown (Tschechische Technische Universit?t in Prag)

Zusammenfassung: Die einfache Typentheorie von Church ist eine Formulierung der Logik h?herer Ordnung, auf der viele interaktive Theorembeweiser beruhen. Ein Vorteil der Verwendung von Churchs Typentheorie ist, dass es für viele Theorien, die keine endliche Axiomatisierung erster Ordnung haben, entsprechende Theorien gibt, die eine endliche Axiomatisierung h?herer Ordnung haben. Ich werde die Churchsche Typentheorie vorstellen und eine endliche Axiomatisierung einer Mengenlehre skizzieren, mit der man Mathematik formalisieren kann. In diesem Zusammenhang werde ich auch das Zusammenspiel von interaktivem Theorembeweisen und automatisiertem Theorembeweisen diskutieren.

Wann: Mi, 16. November, 14:15-15:45

Wo: Erba, Raum WE5/04.004