Termine

Theorie-Kolloquium (3.04.1.02, von 19.10.2010 14:15 bis 19.10.2010 15:45)

Prof.Kreitz, Dienstags 14:15-15:45, 3.04.1.02

19.10. - Diskussion über eine Modifikation des CND-Kalküls (3.04.1.02, von 19.10.2010 14:15 bis 19.10.2010 15:45)

CND ist ein Kalkül für natürliches Schließen in klassischer Logik, der auch als Typisierungsystem für Terme des \lambda\mu-Kalküls dient. Eine konstruktive Einschränkung dieses Kalküls erlaubt nun die Typisierung lediglich für sogenannte "sichere" \lambda\mu-Terme, die auf geschlossene reine \lambda-Terme reduziert werden können...

02.11. Nuria Brede: lambda-mu-PRL - Klassisches Schließen in der konstruktiven Typentheorie (3.04.1.02, von 02.11.2010 14:15 bis 02.11.2010 15:45)

Im Vortrag stelle ich einen Ansatz zur Integration des $\lambda\mu$-Kalküls in die konstruktive Typentheorie des Beweisassistenten Nuprl vor...

09.11. Nuria Brede: lambda-mu-PRL - Klassisches Schließen in der konstruktiven Typentheorie - II (3.04.1.02, von 09.11.2010 14:15 bis 09.11.2010 15:45)

Im Vortrag stelle ich einen Ansatz zur Integration des $\lambda\mu$-Kalküls in die konstruktive Typentheorie des Beweisassistenten Nuprl vor...

16.11. Kirstin Peters, TU Berlin: Über die Ausdrucksstärke des pi-Kalküls (3.04.1.02, von 16.11.2010 14:15 bis 16.11.2010 15:45)

Palamidessi bewies am Beispiel von Leader Election in symmetrischen Netzwerken, dass der pi-Kalkül mit mixed choice ausdrucksstärker ist als der pi-Kalkül mit separate choice. Der Beweis...

30.11. Nuria Brede: lambda-mu-PRL - Klassisches Schließen in der konstruktiven Typentheorie - III (3.04.1.02, von 30.11.2010 14:15 bis 30.11.2010 15:45)

Im Vortrag stelle ich einen Ansatz zur Integration des $\lambda\mu$-Kalküls in die konstruktive Typentheorie des Beweisassistenten Nuprl vor...

11.01. Christoph Kreitz: Global search theory revisited (3.04.1.02, von 11.01.2011 14:15 bis 11.01.2011 15:45)

Im gleichnamigen Preprint von 2010 formuliert Douglas Smith die Theorie der Globalsuch-Algorithmen unter Benutzung der Galoisverbindung von Lösungsmengen und abstrakten Representationen derselben neu.

25.01. Fred Freitas: A Connection Method for Reasoning with the Description Logic ALC (3.04.1.02, von 25.01.2011 14:15 bis 25.01.2011 15:45)

Prof. Frederico Luiz Gonçalves de Freitas Informatics Center - Federal Universidade of Pernambuco (CIn - UFPE), Recife, Brazil On a sabbathical leave at the Knowledge Representation and Knowledge Management Research Group Computer Science Institute, University of Mannheim, Germany

01.02. Christoph Kreitz: Global search theory revisited II (3.04.1.02, von 01.02.2011 14:15 bis 01.02.2011 15:45)

Im gleichnamigen Preprint von 2010 formuliert Douglas Smith die Theorie der Globalsuch-Algorithmen unter Benutzung der Galoisverbindung von Lösungsmengen und abstrakten Representationen derselben neu.

08.02. Thomas Raths: Die QMLTP-Library v1.0 (3.04.1.02, von 08.02.2011 14:15 bis 08.02.2011 15:45)

"Quantified Modal Logic Theorem Proving" (QMLTP)-Library v1.0 - Sammlung von Problemen für Theorembeweiser in modaler Prädikatenlogik.

07.03. Carsten Baum: Grundlagen homomorpher Kryptosysteme (3.04.1.02, von 07.03.2011 11:00 bis 07.03.2011 12:30)

Für manche Anwendungszwecke ist es notwendig, mit verschlüsselten Daten zu rechnen. Dazu definiert man Kryptosysteme, welche homomorph bezüglich der Klartexte sind...