EN | DE
Theoretische Informatik

Themen für Studentische Arbeiten

Wenn Sie eine Bachelor-, Master-, Studien-, Projekt- oder Diplomarbeit bei der Theoretischen Informatik machen wollen, sind Sie hier richtig.

Sie können die Mitarbeiter auch direkt zu Themen ansprechen (wenn Sie beispielsweise einen konkreten anderen Themenwunsch haben).


Fuzzy Description Logic

In der unscharfen Logik (Fuzzy Logic) werden die klassischen Wahrheitswerte “wahr”/“falsch” ersetzt durch Wahrheitsgrade, typischerweise Zahlen zwischen 0 und 1. Über den ursprünglich rein propositionalen Formalismus hinaus gibt es mittlerweile ausdrucksstarke unscharfe Logiken; eine interessante Klasse noch entscheidbarer Logiken dieser Art sind die unscharfen Beschreibungslogiken (Fuzzy Description Logics). Effiziente Deduktionsalgorithmen für Fuzzy DLs werden gerade erst entwickelt, wie etwa dieser hier. Es liegt bereits eine Implementierung eines Tableaualgorithmus für fuzzy ALC vor; mögliche weitere Themen betreffen die systematische Optimierung des Algorithmus und die Erweiterung auf ausdrucksstärkere Logiken.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder


Leichtgewichtige Beschreibungslogik

Leichtgewichtige Beschreibungslogiken zeichnen sich durch geringe Ausdrucksstärke bei gleichzeitiger effizienter Entscheidbarkeit der zentralen Schlussfolgerungsprobleme aus. Die zur Zeit vielleicht erfolgreichste leichtgewichtige Beschreibungslogik ist EL, das auch die in wichtigen großen Ontologien wie SNOMET CT verwendet wird. Wir haben eine koalgebraische Verallgemeinerung von EL entwickelt, in der statt der üblichen relationalen Modalitäten auch z.B. verschiedene spielorientierte Modalitäten verwendet werden können. Ein Reasoner für koalgebraisches EL ist in Vorarbeiten bereits implementiert worden. Als weitere Arbeiten bieten sich systematische Evaluationen sowie eine Erweiterung sowohl der Theorie als auch der Implementierung auf sogenannte general concept inclusions an.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder


Koalgebraisches T

Koalgebraische Modallogik dient als allgemeines Rahmenwerk für Modallogiken jenseits der relationalen Welt, z.B. für probabilistische oder spieltheoretische Modalitäten. Die meisten Resultate in der koalgebraischen Modallogik haben als Gültigkeitsbereich ausschließlich solche Logiken, die, ähnlich wie die Beschreibungslogik ALC bzw. die relationale Modallogik K, nur durch sogenannte Rang-1-Axiome, also solche, in denen alle aussagenlogischen Variablen unter genau einer Modalität stehen, definiert sind (im Falle von K lautet das Axiom [](a→b) → []a → []b). In diesem Projekt soll die Allgemeinheitsebene auf solche Axiome angehoben werden, in denen zwar noch keine geschachtelten Modalitäten, wohl aber Vorkommen von aussagenlogischen Variablen außerhalb von Modaloperatoren erlaubt sind; Grundbeispiel hierfür ist die Modallogik T, die Reflexivität definiert und K um das Axiom []a → a erweitert.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder


Coalgebraic mu-Calculus

Der klassische mu-Kalkül ist ein Formalismus u.a. zur Beschreibung nebenläufiger Systeme. Seine koalgebraische Variante (siehe z.B. hier) deckt in uniformer Weise verschiedene interessante Erweiterungen ab, wie z.B. den alternierenden mu-Kalkül (zur Beschreibung von Agentensystemen) oder den gradierten mu-Kalkül (mit Zähloperatoren, etwa zur Messung von Redundanz). Als theoretische Arbeiten in diesem Gebiet bieten sich die Entwicklung von Modellprüfungsalgorithen (model checker) oder eine Kodierung von Nominalen, also Namen für einzelne Zustände, an.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder


Iron Lambda and Lambda-mu

Iron Lambda is, in its own words, a collection of ​Coq formalisations for functional languages of increasing complexity. It fills part of the gap between the end of the ​Software Foundations course and what appears in current research papers. Recall that our local rendition of the Software Foundations course is Praktische Semantik von Programmiersprachen. The repository does not appear to include formalizations of calculi with continuations and control operators such as those discussed in Chapters 6 and 7 of the Sørensen and Urzyczyn book. The task would be to formalize a chosen example in the style of SF book and/or Iron Lambda repository.

A truly ambitious route would discuss proof term assignment for a proof system involving modalities. This should quickly lead towards a publication on at least solid workshop level. Even pen-and-paper development would involve creativity, there are rather few research-level papers on the subject so far. Details available from Ansprechpartner in person.

Art der Arbeit: This would be more suitable for Master students, but given the quality of some BSc students I've seen here, an ambitious Bachelorarbeit is not out of question.

Ansprechpartner: Tadeusz Litak


Fixpoints in Intuitionistic Propositional Logic

A lot of research attention is devoted to extensions of propositional modal logic and more powerful formalisms with fixpoint operators. This includes even some other projects on this very page. You may ask yourself a question then: would it make sense to add fixpoint operators just to the plain old classical propositional calculus, with no modalities, quantifiers etc.? A quick reflection shows that it would not indeed. Axioms of classical propositional logic make every formula taken as a polynomial in a chosen propositional variable stabilize very quickly. The question how quickly is a good exercise for you to work out on your own… just slightly above the GLoLoP level.

But what if you move to intuitionistic propositional logic, i.e., the system which underlies the Curry-Howard correspondence with functional programming and type systems of proof assistants like Coq? Are all fixpoints still definable with first- or second-order quantifiers, datatypes etc. removed?

It turns out that the answer is yes, but the solution is nowhere near as trivial as for the classical propositional logic. It was found out by Wim Ruitenburg in an unjustly forgotten paper in the 1980's (hat tip to prof. Albert Visser for pointing this one out!). Given how little use has been made from this fact so far, there is potential for several inspiring projects, depending on the needs and expertise of the student:

  • Implement the algorithm, whose description was not entirely transparent in the original paper
  • Formalise a proof of its correctness in Coq
  • Investigate if bounds given in the paper can be improved, at least for some well-behaved subclasses of formulas
  • For a really ambitious student: try to connect this isolated work with the whole body of research on the structure of free Heyting algebras, unification and interpolation issues etc. This path would be certainly at least Master level or above, highly likely leading to scientific publications. Pretty interesting for everybody, I would add.

Art der Arbeit: Any, depending on chosen subproject and the level of difficulty

Ansprechpartner: Tadeusz Litak


Fixpoints in the Logic of Well-Founded Structures

This is a relative of the project above. This time, it has to do with the existence of fixpoints of formulas where every occurrence of a variable is guarded by a modal operator, and this operator is interpreted by a well-founded, transitive relation. That such fixpoints exist is a remarkable fact discovered independently by several logicians in mid-1970's; an account can be found here, for example. This known to work also with the intuitionistic propositional base, see here. There are also nice simplifications possible in special cases, see for example here. Again, the possible tasks are:

  • Implement the algorithm
  • Formalise a proof of its correctness in Coq

Art der Arbeit: Bachelorarbeit oder Masterprojekt. For Masterarbeit we may need to discuss something extra, as theoretical basics seem pretty well investigated, at least as long as one keeps the guardedness assumption. However, allowing a larger class of formulas or more complicated formalisms quickly makes things for more interesting and there are possibilities here to extend the project even above the master level.

Ansprechpartner: Tadeusz Litak


Generalizing Classical Model Theory for CPL

This is a project for students who would enjoy a bit more of old fashioned pen-and-paper work, especially rudiments of model theory which appeared in Logische Grundlagen der Datenbanktheorie. In two conference/workshop papers (ICALP 2012 and TbiLLC 2011) we have proposed Coalgebraic Predicate Logic (CPL): a generic and natural first-order language to reason about such diverse structures as neighbourhood frames, discrete Markov chains, conditional frames, multigraphs and indeed any type of structure that can be understood in terms of Set-coalgebras. Some basic model theoretical results have been proved for this language, but redoing standard, relational model theory in this much broader setting remains a large task to be completed. It would also generalize a lot of work on topological model theory done by several research centers in Germany in 1970's or 1980's. Some examples of nice, relatively easy warm-up questions have been already suggested in the ICALP paper: obtaining Hilbert-style completeness for some non-compact (but omega-bounded) structures using an omega-rule or investigate a generalization of the omitting types theorem. More challenging ones would include: Beth definability or interpolation, a Keisler-Shelah characterization theorem or a Herbrand theorem.

Art der Arbeit: Any, depending on chosen subproject and the level of difficulty

Ansprechpartner: Tadeusz Litak


Formalizing Relational Lattices In Coq

Relational lattices provide an algebraic framework for database theory suggested first by Vadim Tropashko from Oracle. While the inventor of relational lattices produced a dedicated tool, the option of formalizing their metatheory in a generic theorem prover like Coq, Agda or Isabelle using the insights of our RAMiCS 2014 paper remains both viable and tempting: there are still too many open questions that may be hard to attack otherwise. This project could be enjoyable to veterans of SemProg and/or those of LGruDat.

Art der Arbeit: This would be more suitable for Master students, but given the quality of some BSc students I've seen here, an ambitious Bachelorarbeit is not out of question.

Ansprechpartner: Tadeusz Litak


From Prover9 to Modern Proof Assistants

Prover9 is a rather useful automatic theorem prover whose developer sadly perished in 2009 and since then its development has been frozen. It is rather powerful and still used occasionally (also by me), but apart from the obvious issue of bugs not being fixed and code being increasingly out of date, its output is not particularly readable. A big challenge (which may take more than work of one student…) would be to find an automatic way of translating at least a subclass of proofs generated by Prover9 to proof scripts that can be verified by Isabelle or Coq, thus saving them from the fate of legacy code.

Art der Arbeit: This would be more suitable for Master students, but given the quality of some BSc students I've seen here, an ambitious Bachelorarbeit is not out of question.

Ansprechpartner: Tadeusz Litak