Logo Leibniz Universität Hannover
Logo:Institut für Theoretische Informatik
Logo Leibniz Universität Hannover
Logo:Institut für Theoretische Informatik
  • Zielgruppen
  • Suche
 

Themenübersicht Abschlussarbeiten

Wenn Sie an anderen Themen interessiert sind oder eigene Vorschläge haben, wenden Sie sich bitte an einen unserer Mitarbeiter. Prinzipiell kann jedes Thema im Umfang angepasst werden, sodass es für eine Bachelor-, Master- oder Diplomarbeit passend ist.

Algorithmen

Komplexitätstheorie

On Satisfiability Problems with a Linear Structure

Eine neue Einschränkung an das Erfüllbarkeitsproblem, die zu effizienten Algorithmen führt, wurde kürzlich von Gaspers et al. eingeführt. Die Resultate sollen nachvollzogen und weiterentwickelt werden.
Literatur: Serge Gaspers, Christos Papadimitriou, Sigve Hortemo Saether, Jan Arne Telle, On Satisfiability Problems with a Linear Structure, arXiV 1602.07876.

Vollmer

Maschinengrößen

In einem Blog-Eintrag von Gasarch wird über sogenannte Bounding Functions referiert. Eine Funktion f nennt man eine Bounding Function für zwei Maschinentypen (D, E), wenn eine Sprache L durch eine D- und E-Maschine akzeptiert werden kann und L von der E-Maschine der Größe n akzeptiert wird, dann kann L von einer E-Maschine der Größe höchstens f(n) akzeptiert werden.

In der Arbeit sollen die Resultate bzgl. DEA, NEA, DKA, NKA und LBA erläutert und in Bezug zueinander gesetzt werden. Hierzu gibt es in dem Blog-Eintrag Verweise auf Original-Literatur.

Meier

Catalytic Space

Eine neue Art, Speicherbedarf zu messen, würde kürzlich unter der Bezeichnung “katalytischer Speicher” untersucht. Dabei handelt es sich um Speicher, der für Zwischenrechnungen benutzt werden darf, aber danach wieder den ursprünglichen Inhalt aufweisen muss. Es geht also um die Frage, ob Speicher, der bereits Daten enthält, die erhalten bleiben müssen, dennoch für Berechnungen genutzt werden kann. Interessante komplexitätstheoretische Resultate sind bekannt, die zusammengefasst werden sollen.

 

Link: Catalytic Space http://bulletin.eatcs.org/index.php/beatcs/article/view/400

Vollmer

Quantum Interactive Proof Systems

In dieser Arbeit geht es darum Quantum Interaktive Beweissysteme darzustellen, sowie die Beweisideen zu präsentieren, die zeigen, dass die Klasse QIP mit PSPACE zusammenfällt. Hierzu wird außerdem auf Arthur-Merlin Spiele eingegangen und ihr Zusammenhang zu den Quantum Interaktiven Beweissystemen dargestellt.

Siehe auch:

Meier

Minimale Schaltkreise

Das Problem der minimalen Schaltkreisgröße MCSP ist eines der wenigen bekannten Probleme aus der Klasse NP, von denen weder bekannt ist, ob es NP-vollständig ist, noch, ob es in Polynomialzeit lösbar ist. Es gehört also zu den sog. ``intermeidate problems’’. Die bekannten Komplexitätsresultate über MCSP sollen zusammengefasst werden.

 

Link: Complexity of Complexity http://link.springer.com/chapter/10.1007%2F978-3-319-50062-1_6

Vollmer

New circuit lower bound I

Kürzlich wurde in einer Arbeit von R. Williams die Komplexitätsklasse ACC von NEXPTIME getrennt. Der Beweis soll nachvollzogen werden.

Siehe auch: Gödels Lost Letter

Vollmer

New circuit lower bound II

Die Permanente ist eine Eigenschaft von Matrizen und ist ganz ähnlich zur Determinante definiert, weist aber interessanterweise sehr unterschiedliche Komplexitätseigenschaften auf. Die bestehenden Resultate über die Komplexität der Permanente sollen zusammengefasst werden.

Vollmer

Komplexität der Theorie der reellen Zahlen

Die Theorie der reellen Zahlen ist im Gegensatz zur Theorie der ganzen Zahlen, der sog. elementaren Arithmetik, entscheidbar. Die wesentlichen Aussagen zu Entscheidbarkeit und Komplexität sollen zusammengefasst werden.

 

Link: Existential Theory of the Reals https://en.wikipedia.org/wiki/Existential_theory_of_the_reals

Vollmer

Komplexität von Datenkompression

Bekannte Kompressionsalgorithmen wie die von Lempel und Ziv oder Huffman berechnen aus einem Eingabewort ein im Allgemeinen kürzeres Wort, aus dem sich das Originalwort rekonstruieren lässt. Die Theorie der sog. Kolmogorov-Komplexität zeigt Möglichkeiten und Grenzen solcher verlustfreier Kompressionsalgorithmen auf, die in dieser Arbeit nachvollzogen werden sollen.

 

Link: Compression Complexity https://arxiv.org/abs/1702.04779

Vollmer

Beliebte Spiele sind schwierig: Schach, Go, Halma und 2048.

Viele beliebte (Gesellschafts-)Spiele haben verallgemeinert eine hohe Komplexität: Schach ist EXPTIME-vollständig, Go und Halma sind EXPSPACE-vollständig, 2048 ist PSPACE-schwer. In dieser Arbeit sollen die Beweisideen herausgearbeitet, sowie Gemeinsamkeiten zwischen den unterschiedlichen Resultaten gefunden werden. 

Siehe auch:

Meier

Kryptographie

Obfuskation und Kryptographie

Obfuskation ist die absichtliche des Quellcodes eines Programms, sodass die Funktionalität erhalten bleibt, aber der Code für Menschen schwerer lesbar wird. In einer Reihe neuerer Arbeiten werden interessante Konsequenzen in der Kryptographie aufgezeigt.

Literatur:
C. Brzuska, P. Farshim, A. Mittelbach: Indistinguishability Obfuscation and UCEs: The Case of Computationally Unpredictable Sources, Advances in Cryptology – CRYPTO 2014, Volume 8616 of the series Lecture Notes in Computer Science pp 188-205

Vollmer

Berechenbarkeit

Zufallszahlen in der Berechenbarkeitstheorie

Als Zufallszahlen werden Zahlen bezeichnet, die nicht komprimierbar sind, d. h., kein Algorithmus kann mehr Stellen der Zahl wiedergeben, als seine eigene Länge beträgt. Ein Beispiel sind die Chaitinschen Konstanten, gelegentlich "Zahlen der Weisheit" genannt. Die Existenz von Zufallszahlen hat weitreichende Konsequenzen in der Theorie der Berechenbarkeit und der formalen Beweissysteme.

Vollmer, Lück

Logik

Prädikatenlogik der zweiten Stufe

In der Prädikatenlogik der zweiten Stufe sind neben den “gewöhnlichen” Quantoren auch Quantoren über Relationsvariablen erlaubt. Diese Arbeit soll einen Überblick über diese Logik geben.

 

Link: Second-order and Higher-order Logic http://plato.stanford.edu/entries/logic-higher-order/

Vollmer

Nichtmonotone Logiken

Schlussfolgerungen im Alltag sind oft von der Art, dass Folgerungen bei Bekanntwerden neuer Fakten zurückgezogen werden müssen. Dies widerspricht der Monotonie formaler Logiken, bei denen die Hinzunahme von zusätzlichen Axiomen bisherige Schlüsse nicht ungültig macht.

 

Mögliche Themen für Abschlussarbeiten aus diesem Bereich sind:

 

Eine spezielle Form der nicht-monotonen Logik ist die sog. autoepistemische Logik, über die ein Überblick verfasst werden soll.

Link: Non-monotonic Logic http://plato.stanford.edu/entries/logic-nonmonotonic/

 

Die Komplexität des Erfüllbarkeitsproblems für nicht-monotone Logiken soll untersucht werden.

 

Link: Complexity Results for Nonmonotonic Logics  logcom.oxfordjournals.org/content/2/3/397.full.pdf

Vollmer

Modallogische Systeme

Wie in der Vorlesung “Logik und Formale Systeme” gezeigt, lassen sich bestimmte Eigenschaften von Kripke-Strukturen, wie Symmetrie oder Transitivität, durch modallogische Axiome beschrieben werden. Diese sog. Korrespondenztheorie soll mittels eines Lehrbuchs der Modallogik aufgearbeitet werden.

 

Link: Modal Logic https://plato.stanford.edu/entries/logic-modal/, Abschnitt 8 und 9

Vollmer

Resolution für Modallogik

Die aus der Aussagenlogik bekannte Methode der Resolution kann auf Modallogik erweitert werden. Das Verfahren soll dargestellt werden.

 

Link: Modal Resolution in Clausal Form http://www.sciencedirect.com/science/article/pii/0304397589901370

Vollmer

Logische Grundlagen der Programmiersprache PROLOG

Der PROLOG-Interpreter ist im wesentlichen ein Verfahren der sog. SLD-Resolution. Die logischen Grundlagen der Programmiersprache sollen dargestellt werden.

 

Link: SLD Resolution https://en.wikipedia.org/wiki/SLD_resolution

Vollmer

Unabhängigkeitsresultate

Viele Beziehungen zwischen Komplexitätsklassen sind trotz jahrzehntelanger Forschungen noch ungeklärt; am bekanntesten ist das P-NP-Problem, also die Frage, ob die Klassen P und NP zusammenfallen. In der Logik wurde die Frage untersucht, ob das P-NP-Problem und weitere offene Fragen vielleicht gar nicht mit mathematisch-logischen Mitteln gelöst werden können. Aussagen, die in einer bestimmten logischen Theorie weder bewiesen noch widerlegt werden können, nennt man <i>unabhängig</i> von der Theorie. Erstaunlich einfache Unabhängigkeitsresultate sind bekannt. In dieser Arbeit soll ein Überblick über diese Untersuchungen gegeben werden.

 

Link: A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory https://arxiv.org/abs/1605.04343

Vollmer

Konstruktive Mengen

In der mathematischen Logik wurden konstruktive Mengen von Kurt Gödel eingeführt. Grob gesprochen lassen sie sich induktiv durch einfache Operationen definieren. In dieser Arbeit sollen mögliche Anwendungen konstruktiver Mengen in der Komplexitätstheorie untersucht werden.

Siehe auch: Gödel's Lost Letter

Vollmer

Endliche Modelleigenschaft in modaler Logik

Endliche Modelleigenschaften spielen in modalen Logiken eine entschiedene Rolle in Fragestellungen bezüglich Komplexität und Entscheidbarkeit. Endliche Modelleigenschaften können durch verschiedene Techniken bewiesen werden. In dieser Arbeit sollen die Filtrations-, sowie die Selektionstechnik untersucht und dargestellt werden.

Siehe auch Shethmann, Filtration via bisimulation, 2004.

Vollmer

Formale Sprachen

Eine Logik mit zwei Variablen

Eine neue Spezifikationssprache für formale Sprachen, die auf Logik mit zwei Variablen beruht, wurde kürzlich von Krebs et al. eingeführt. Die Resultate sollen nachvollzogen werden. Anhand von konkreten Beispielen soll die Ausdrucksfähigkeit der neuen Sprache untersucht werden.
Literatur: Andreas Krebs, Kamal Lodaya, Paritosh Pandya, Howard Straubing, Two-variable Logic with a Between Predicate, arXiV 1603.05625.

Vollmer

Äquivalenz von DPDAs

Die Äquivalenz von deterministischen Kellerautomaten ist entscheidbar. Der Beweis soll nachvollzogen werden.

Vollmer

Sonstige Themen

Der akademische Arbeitsplatz

  • In einer Fallstudie soll der Einsatz von Tools wie DEVONthink, Sente, Scrivener etc. im Workflow eines Akademikers untersucht werden.
  • Eine SVN-App für das iPad soll entwickelt werden.

Vollmer