Open Student Projects

The following websites list severals topics for student projects (Bachelor's or Master's Level)

• Topics related to higher-order automated theorem proving and the LEO-II project
• Topics related to the ontology project SUMO – these topics will be supervised in collaboration with Articulate Software, Angwin, CA, USA
• more to come ...

PhD topics are not listed here; they will be discussed more closely on an individual basis.

PhD students

• Marvin Schiller: Granularity Analysis for Tutoring Mathematical Proofs (ongoing, funded by Studienstiftung des Deutschen Volkes).
• Frank Theiss: Higher Order Term Indexing (ongoing).
• Marc Wagner, Dominik Dietrich, Mark Buckley (I was involved at an earlier phase of their PhD projects).
• Axel Schairer: Transformations of specifications and proofs to support an evolutionary formal software development (completed, I was involved as ”wissenschaftlicher Begleiter”).
• Jürgen Zimmer: MathServe – A Framework for Semantic Reasoning Services (completed).
• Volker Sorge: A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning (completed).

PhD Committee member

• Stefano Zacchiroli, User Interaction Widgets for Interactive Theorem Proving, Unversity of Bologna, Italy, 2007.
• Tim Priesnitz: Subtype Satisfiability and Entailmant, 2005.
• Volker Sorge: A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning, 2001.
• Armin Fiedler: User-Adaptive Proof Explanation, 2001.

MSc/BSc/Diploma projects (Supervised, Co-Supervised, or Reviewed)

• Yecheng Gu (Bachelor): Integration of Rippling into the Omega System, (completed) 2009.
• Jonathan Osthof (Bachelor): Orchestriation of Distributed Strategies in Interactive and Automated Theorem Proving (completed). 2008.
• Valentin Dimitrov (Diplom, only Assessment): UbiSpot: An In- and Outdoor Positioning Client for Symbian OS (completed). 2008.
• Stephanie Ehrbächer (Bachelor): Application of the Frame-based Mathematical Database MaKE in Proof Planning (completed). 2007.
• Ali Rahmani (Bachelor, only Assessment): Graphische Darstellung eines Tagessollplanes (completed). 2007.
• Can Kayali (Bachelor): Assertion Level Proofs with Underspecification (completed). 2006.
• Robert Vollmann (Bachelor): Implementation of a Scalable GameMaster to Illustrate and Evaluate AI Techniques (completed). 2006.
• Dominik Dietrich (Diplom): Multi-Strategy Proof-Planning based on CORE (completed). 2006.
• Marc Wagner (Diplom): Abstract Verification of Mathematical Proofs (completed). 2006.
• Marc Buckley (Diplom): An Agent-oriented Approach to Dialog Managment (completed). 2005.
• Syed Sajjad Hussain (Master, only Assessment): Unknown (completed). 2005.
• Marvin Schiller (Diplom): Tutorial Proof Step Evaluation wrt Granularity and Relevance (completed). 2005.
• Frank Theiss (Diplom): On the White Box Integration of Computer Algebra Algorithms into a Deduction System (completed). 2005.
• Eugen Staab (Masters): BDI Agenten zur Modellierung des Lieferkettenmanagements in der Stahlproduktion (completed). 2005.
• Stephanie Ehrbächer (Bachelor): Term Data Structures and Theory Unification for a Frame-based Mathematical Database (completed). 2005.
• Andreas Franke (Diplom): Inhaltsorientierte Verwaltung mathematischen Wissens (completed). 2003.
• Malte Hübner (Diplom): Interactive Theorem Proving with Indexed Formulas (completed). 2003.
• Stephan Hess (Diplom): Software-Ergonomie in einer Beweisentwicklungsumgebung (completed). 1999.
• Lars Klein (Diplom): Indexing fuer Terme höoeherer Stufe (completed). 1997.
• Ahmet Bozkurt (Diplom): Strategien für Resolutionsbeweiser in Logik höherer Stufe (completed). 1995.