Prerequisites: basic knowledge of the Mathematica programming language and LaTeX, interest in writing/formating mathematical documents, working in a bigger team, and structured software development.

Working area: 50% mathematics, 50% informatics.

Skip to content
## Open Topics

Theorema Project: Document Processing (Advisor: Wolfgang Windsteiger). The task in this thesis is to setup an environment for preparing entire (big) mathematical documents in Theorema 2.0. This comprises the design of appropriate Mathematica stylesheets and a mechanism for translating Mathematica notebooks into nicely formatted LaTeX documents Formalization of Elementary Parts of Mathematics (Advisor: Wolfgang Windsteiger).
Prerequisites: Interest in working in computer-supported mathematics, basic understanding of logic.
Working area: 100% mathematics, 0% informatics. RISC Algorithm Language (Advisor: Wolfgang Schreiner). Algorithm Synthesis (Advisor: Tudor Jebelean) Automated Reasoning in Natural Style (Advisor: Tudor Jebelean) Case Studies of Reasoning in Elementary Analysis (Advisor: Tudor Jebelean) Computer algebra for algebraic differential equations (explicit formula solutions for algebraic DEs) (Advisor: Franz Winkler) Efficient Proposational Proving (Advisor: Tudor Jebelean) Further development and use of the unification and generalization algorithm library (Advisor: Teimuraz Kutsia). At RISC, we have been developing an open source library of unification and generalization algorithms, currently hosted at
http://www.risc.jku.at/projects/stout/
Unification is a process of equation solving, aiming at computing a most general common instance of the terms involved. Anti-unification is its dual process, aiming at computing a least general common generalization of the input terms (retaining their common structure as much as possible).
The topics are for one or more bachelor theses: Extend the library by
implementing recently developed improvements of some of the algorithms already in the library; add a new algorithm for term-graph generalization; add an algorithm for context sequence matching with regular constraints; experimental applications.
Prerequisites: Programming in Java (since the library is written in Java), basic knowledge of logic, some familiarity with declarative programming and automated reasoning is a plus. Modulare Funktionen im Computeralgebra System SAGE (Advisor: Peter Paule) Multiview Geometry (Advisor: Josef Schicho) Program Testing and Verification (Advisor: Tudor Jebelean) Symbolic computation and positivity of holonomic sequences (Advisor: Veronika Pillwein). Around ten years ago Stefan Gerhold and Manuel Kauers developed a symbolic method to show positivity for sequences defined by a linear recurrence relation with polynomial coefficients. More recently, in the course of a termination analysis, a variation of this method has been introduced. The goal of this thesis is to implement this new procedure in Mathematica and compare its behaviour at some practical examples with the existing implementation of the Gerhold-Kauers method. Visualisierung von komplexer Analysis im System Mathematica (Advisor: Peter Paule) Die Newton-Andrews-Zeilberger Methode zur Berechnung von harmonischen Summen Identitäten (Advisor: Carsten Schneider) Gelenkmechanismen (Advisor: Josef Schicho). Man konstruiere Familien von Bennett-Mechanismen, die eine vollständige Drehung ohne Kollisionen zulassen. Hamilton-Mechanik (Advisor: Josef Schicho). Man beschreibe die Bewegung zweier fester Körper, die durch ein Drehgelenk miteinander verbunden sind, ohne Einwirkung äußerer Kräfte. Lösen von algebraischen Gleichungen mit speziellen Funktionen (Advisor: Peter Paule) ### Theorema Project: Design and Implementation of a Test Environment

Theorema Project: Design and Implementation of a Test Environment (Advisor: Wolfgang Windsteiger). The topic of this thesis is the design and implementation of a unit testing environment for the Theorema development. When new components are added to the system, a certain set of tests should be run automatically and some statistics about how many tests have been passed should be generated.Theorema Project: Specialized Proving Methods (Advisor: Wolfgang Windsteiger). In the frame of this thesis, specialized proving/solving tequniques for particular areas of mathematics (e.g. polynomials, vector spaces, etc.) should be studied and implemented in the frame of Theorema 2.0.
Prerequisites: basic knowledge of the Mathematica programming language, interest in logic/proving, working in a bigger team, and structured software development.
Working area: 80% mathematics, 20% informatics. Theorema Project: Interactive Proving (Advisor: Wolfgang Windsteiger). The topic of this thesis is the design and implementation of an interactive theorem prover in the frame of Theorema 2.0.
Prerequisites: basic knowledge of the Mathematica programming language, interest in logic/proving, working in a bigger team, and structured software development.
Working area: 50% mathematics, 50% informatics. RISC Algorithm Language (Advisor: Wolfgang Schreiner). ## Theses in Progress

Theorema Project: Tracing Computations (Advisor: Wolfgang Windsteiger). The Theorema system displays mathematical proofs in natural language in a structured way, such that every logical step can easily be understood by humans. In this thesis, a similar mechanism should be developed for computations, such that calculations are presented step-by-step in a human-comprehensible way. ### Implementation of symbolic geometric method for rational solutions of AODEs

Implementation of symbolic geometric method for rational solutions of AODEs (Advisor: Franz Winkler)### Radu’s Ramanujan-Kolberg Algorithm in Mathematica

Radu's Ramanujan-Kolberg Algorithm in Mathematica (Advisor: Peter Paule)### Formal Design Method For Reasoning about Algorithms and Representing Efficient Programs

Formal Design Method For Reasoning about Algorithms and Representing Efficient Programs (Advisor: Tudor Jebelean)### Difference Ring Algorithms for Nested Products

Difference Ring Algorithms for Nested Products (Advisor: Carsten Schneider). We develop algorithms to represent nested products over hypergeometrics, q-hypergeometric, multibasic and mixed hypergeometric expressions in difference rings.

Prerequisites: basic knowledge of the Mathematica programming language and LaTeX, interest in writing/formating mathematical documents, working in a bigger team, and structured software development.

Working area: 50% mathematics, 50% informatics.

Master Thesis

Advisor: Wolfgang Windsteiger

Prerequisites: basic knowledge of the Mathematica programming language, working in a bigger team, and structured software development.

Working area: 10% mathematics, 90% informatics.

Master Thesis

Advisor: Franz Winkler

Investigator: Fabrizio Zucca

Master Thesis

Advisor: Peter Paule

Investigator: Bernhard Kepplinger

PhD Thesis

Advisor: Tudor Jebelean

Investigator: Jakob Praher

PhD Thesis

Advisor: Carsten Schneider

Investigator: Evans Doe Ocansey