Jobs

Available Master Theses

• Termination-Analysis as Proof Strategy in OMEGA
  Supervisor: Serge Autexier, Dominik Dietrich
  
• TRAMP4OMEGA: Transformations of Refutation Proofs in First-Order Logic into Proofs of the Mathematical Assistance System OMEGA
  Supervisor: Serge Autexier, Dominik Dietrich
• Extending CORE by Descente Infinie
  Supervisors: Serge Autexier, Claus-Peter Wirth
• Formalization of Mathematical Texts in PLATO/OMEGA
  Supervisor: Dominik Dietrich, Marc Wagner
  Formalization of parts of typical mathematical theories like Number Theory, Real Analysis, Group Theory and Category Theory (or other mathematical areas) in the text-editor TEXMACS and in interaction with the Mathematical Assistant System PLATO/OMEGA.
• TRAMP4HOL: Transformations of Refutation Proofs in Higher-Order Logic into OMEGA Proofs
  Supervisor: Serge Autexier, Christoph Benzmüller
• Paramodulation/Superposition based Calculi for Higher-Order Logic
  Supervisor: Christoph Benzmüller
• Mapping of First-Order Representations of Mathematics into Higher-Order Representations
  Supervisor: Christoph Benzmüller
• Higher-Order Representations with Product-Types (and Dependent-Types) vs. Representations in Simply Typed Lambda-Calculus
  Supervisor: Christoph Benzmüller
• Transformational Approach to Evolutionary Formal Development based on MAYA and CORE
  Supervisors: Serge Autexier, Dieter Hutter
• Extension of Superposition to Non-normalform Resolution and Paramodulation
  Supervisor: Serge Autexier

Completed Master and Diploma Theses

• Mediation between Text-Editors and Proof Assistants
  Student: Marc Wagner
  Supervisors: Serge Autexier, Christoph Benzmüller
• The Task-Layer of the OMEGA System
  Student: Dominik Dietrich
  Supervisors: Serge Autexier, Christoph Benzmüller, Andreas Meier
• Semantics-based Diff, Patch & Merge for XML-Documents
  Student: Svetlana Radzevich
  Supervisor: Serge Autexier, Dieter Hutter
• Intelligent Tutoring Systems in the field of Mathematical Proof
  Student: Marvin Schiller
  Supervisor: Christoph Benzmüller

Available Bachelor Theses

• Implementation of a MS Word Plugin for collaborative mathematical authoring
  Supervisor: Marc Wagner
  
• Lemma Generalisation Heuristics in OMEGA
  Supervisor: Serge Autexier, Dominik Dietrich
  
• Decision procedures for Decidable Theories as Proof Strategies in OMEGA
  Supervisor: Serge Autexier, Dominik Dietrich
  
• Registering the Higher-Order Theorem Prover LEO for the QPQ Library
  Supervisor: Christoph Benzmüller
• Re-implementation of MAYA parameterised over logics and theory contents + Management of Change
Supervisors: Serge Autexier, Dieter Hutter

Completed Bachelor Theses and FoPras

• Implementation of a parameterized incremental parser for TeXmacs formulas
  Student: Thomas Neumann
  Supervisor: Serge Autexier
• Higher-Order Rippling
  Student: Steffen Metzger
  Supervisors: Serge Autexier, Dieter Hutter
• Implementation of a scalable GameMaster to illustrate and evaluate AI Techniques
  Student: Robert Vollmann
  Supervisors: Serge Autexier, Christoph Benzmüller
• Simulationsumgebung für formal spezifizierte Agenten-Systeme
  Student: Hichem Haraketi
  Supervisors: Serge Autexier, Dieter Hutter
• Assertion-level Proof Representation with Under-Specification
  Student: Can Kayali
  Supervisors: Serge Autexier, Armin Fiedler
• Calculus-Independent Hierarchical Proof Datastructure
  Student: Dominik Dietrich
  Supervisors: Serge Autexier, Christoph Benzmüller