Direkt zum Inhalt | Direkt zur Navigation

Sektionen
Benutzerspezifische Werkzeuge

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.

The automation of single non-classical logics is already very challenging. This is particularly true for expressive non-classical logics such as quantified modal logics. Largely unsolved is the question, whether flexible combinations of expressive classical and non-classical logics can be mechanized and automated in a generic framework. This question is relevant beyond the boundaries of computer science and artificial intelligence.

In my talk I will outline a solution based on classical higher order logic. I will show that many non-classical logics are just natural fragments of classical higher order logic. Hence, also combinations of these logic fragments can be easily modeled in higher order logic. A particular focus of the talk will be on quantified modal logics and their combinations.

Employing the above approach off-the-shelf higher order automated theorem provers, like my own LEO-II system, and higher order model finders can be directly applied for reasoning within non-classical logics and their combinations. Interestingly, even automated verification and exploration of meta-level properties of logics and logic combinations is now feasible.

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

 

Artikelaktionen
Auf einen Blick
Lehrform Oberseminar
Empfohlen ab FS 6
Voraussetzungen

Aktive Mitarbeit an Themen der Arbeitsgruppe, z.B zur Vorbereitung und Präsentation von Studien- und Abschlussarbeiten. Keine Doppelanrechnung von eigenständiger Leistung.

Benotet Ja
Punkte gesamt 3
davon praktisch 3
Sprache deutsch
Fremdhörer zugelassen? Nein
Teilgebiete Theoretische Informatik(2000), Angewandte Informatik(4000)
Studiengang Bachelor, Master
Belegung via PULS