Theorie-Kolloquium
- Oberseminar, Prof. Dr. Kreitz, Dr. rer. nat. Richter, Di. 14:00-16:00, 3.04.2.01
In unserem Kolloquium diskutieren wir aktuelle Forschungsprojekte und -ergebnisse unserer Arbeitsgruppe und für unsere Arbeit relevante Ergebnisse aus den Bereichen Formale Methoden in der Programmierung sowie automatisches und taktikbasiertes Theorembeweisen.
Vorträge
wann |
was |
wer |
---|---|---|
31.01.2012 |
Parsing jenseits von kontextfreien Grammatiken Da kontextfreie Grammatiken natürliche Sprache nicht adequat beschreiben können, sind berechenbare Grammatikformalismen, die über CFG hinausgehen, von großem Interesse in der Computerlinguistik. Der Vortrag soll zum einen die Grenzen der generativen Potenz der CFG in Bezug auf natürliche Sprache aufzeigen. Zum anderen werden wir diese Grenzen überschreitende Formalismen vorstellen und bezüglich Mächtigkeit und Komplexität in bekannte Systeme einordnen. |
Anna Melzer |
15.11.2011 |
Automating Expressive Non-classical Logics and their Combinations in Classical Higher Order Logic As an alternative or as an extension to classical logics,
non-classical logics play an increasingly important role in computer
science and related fields. |
Christoph Benzmüller (FU Berlin) |
08.11.2011 |
Homotopietheoretische Modelle intentionaler Typentheorie
Wir diskutieren die verschiedene Ansätze zu einer Homotopietheoretischen Interpretation intentionaler Martin-Löf Typentheorie. Insbesondere werden "weak factorization systems" und einige andere relevante Konzepte aus der Theorie der Modellkategorien vorgestellt und an Beispielen erläutert. |
Tim Richter |
25.10.2011 |
Was ist ein Beweis? Wie beweist man gegenüber einer Person eine Aussage? Ausgehend von diesen Fragen soll das Gebiet der sogenannten 'Interaktiven Beweise' eingeführt werden. Diese bieten die Möglichkeit, mit kryptographischer Sicherheit Beweise gegenüber einem Verifizierer unter gewissen Bedingungen zu führen. Man kann als Bedingung beispielsweise fordern, dass der Verifizierer aus dem Beweis nichts Neues lernen kann (außer dass die Aussage wahr ist). Ein Großteil der dafür verwendeten Protokolle soll anschließend mit einem einzigen Theorem bewiesen werden. |
Carsten Baum |