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.
26.02.2013 Mario Frank: "Formelselektion in großen Formelsammlungen ohne Nutzung der Formelstruktur"
Der Vortrag beschäftigt sich mit der Konnektionssuche in großen
Formelsammlungen der Prädikatenlogik erster Ordnung mit
Repräsentation des Such-Ergebnisses als Graph.
Dabei werden sowohl Aspekte der Vorverarbeitung der Dateien und Formeln
(Parsing, Normalform-Transformation, Gleichheits-Hüllen, Metriken),
als auch die Suche an sich (Unifikation, Initial-Konnektion,
Pfaderweiterung) behandelt und die Unterschiede zu dem Suchverfahren von
ARDE dargelegt.
Donnerstag, 7.2. 12:15 im Raum
S 26 (während der Vorlesung "Kryptografie")
Robert Bär: Vorstellung der Diplomarbeit
"Supersingulare elliptische Kurven in der Kryptografie"
Diese Arbeit beschäftigt sich mit supersingularen elliptischen Kurven in der Kryptographie. Neben
einer Definition von supersingularen elliptischen Kurven wird Schoof's Algorithmus zum Zählen der
Punkte einer elliptischen Kurve vorgestellt, um diese zu finden. Weiter wird die Weil Paarung
eingeführt, welche die Grundlage für den MOV Angriff auf das diskrete Logarithmus-Problem in
elliptischen Kurven bildet. Dieser ist besonders wirksam bei supersingularen elliptischen Kurven und
macht sie dadurch ungeeignet für die Elliptic Curve Cryptography. Die Weil Paarung bildet ebenfalls
die Grundlage für eine drei Parteien Variante des Diffie Hellman Schlüssellaustausches, welche
praktisch allerdings wenig Anwendung findet. Abschließend wird ein identitätsbasierendes
Kryptosystem mit zentraler Instanz vorgestellt, auch hier bildet die Weil Paarung die Grundlage.
Freitag, 01.02.2012, 14.30 Uhr, Raum 2.01
Carsten Baum: Vorstellung der Diplomarbeit:
"Parameter Choices for a Somewhat Homomorphic Encryption Scheme in a Multiparty Computation setting"
Homomorphe Verschlüsselungssysteme haben in der Kryptographie eine breite Anwendung gefunden. Ein solches Verschlüsselungsverfahrens wird als Bestandteil eines kryptographischen Protokolls von Smart, Pastro, Damgard und Zakarias benutzt.
Im Vortrag werden das kryptographische Protokoll sowie das Verschlüsselungsverfahren skizziert und mögliche Optimierungen vorgestellt.
Es wird weiterhin auf asymptotische Schranken für die Parameter des Verschlüsselungsverfahrens eingegangen.
22.01.2013 Eva Richter: "Fuzzy Kernel Revision"
Im Bereich der Überzeugungsrevision gibt es zwei verschiedene Ansätze: partial meet revision und kernel revision.
Im Unterschied zur partial meet revision lässt sich die Idee der
kernel revision nicht ohne weiteres auf die Situation der abstrakten
Fuzzy-Logik übertragen.
Im Vortrag stellen wir die beiden Ansätze der Überzeugungsrevision
für klassische Logik dar, geben einen Überblick über abstrakte
Fuzzy-Logik und erläutern die Probleme sowie einige Lösungsansätze für
Fuzzy-Überzeugungsrevision.
11.12.2012 Sebastian Böhne: "Russells verzweigte Typentheorie (RTT) im modernen Gewande."
- Kurze Wiederholung und Klassifikation von verschiedenen Paradoxa als Grundmotivation für RTT.
-
- Formale Definition von Aussagefunktionen.
- Eine mögliche Übersetzung in den Lambda-Kalkül.
- Typen in RTT: Eigenschaften und Probleme
- Ordnungen, ein unnötiges Hindernis?
- Abriss einfache Typentheorie (STT)
- Idee von Kripkes Wahrheitstheorie (KTT)
- Verbindungen zu NUPRL
30.10.2012 Mario Frank: "Pushing limits of automated theorem provers: Axiom Relevance Decision Engine"
Automatische Deduktion (automated theorem proving) hat in den letzten Dekaden in den verschiedensten wissenschaftlichen Bereichen Einzug gehalten und unterstützt beispielsweise den Beweis der Sicherheitseigenschaften von Netzwerkprotokollen und die Lösung von linguistischen oder medizinischen Fragestellungen.
Viele interessante Probleme enthalten jedoch so große Formelmengen, dass die Beweissysteme an ihre technischen Grenzen stoßen und die Beweissuche nicht mehr in akzeptabler Zeit möglich ist. Im Vortrag wird ein Unifikationsbasiertes Konzept zur Verringerung der Formelmenge vorgestellt und dessen Implementierung beleuchtet.
16.10.2012 Anna Melzer: "Baumautomaten"
operieren, operieren Baumautomaten auf Bäumen. Obwohl sie auf komplexeren Datenstrukturen operieren, zeichnen sich Baumautomaten durch ähnlich wünschenswerte Berechnungseigenschaften aus wie endliche Automaten. Der Vortrag gibt eine Einführung in die theoretischen Grundlagen und einen Ausblick auf Anwendungsmöglichkeiten in der Praxis.
