The RISC Curriculum in Symbolic Computation

Research Topics

Within the realm of symbolic computation, research at RISC mainly falls into three general categories:

Computer Algebra

We design and implement algorithms that operate on algebraic expressions; typical application areas are e.g. (algebraic) geometry and (algorithmic) combinatorics.

Computational Logic

We work on the specification, management, and derivation of knowledge expressed in the language of symbolic logic (resulting in software systems for supporting mathematical proving) and on the theory of computation.

Mathematical Software

We develop various symbolic computation software such as it occurs in computer algebra systems and theorem provers and study the logical foundations of software for the purpose of formal system specification and verification.

These categories (which present different views to the same field with strong overlappings and interrelationships) are also reflected in the RISC curriculum.

See below for a description of various research topics pursued at RISC.

Computer Algebra for Differential Equations

Algebraic differential equations can be treated by symbolic geometric methods. Parametrization of algebraic varieties leads to solutions of the corresponding differential equation.

Algorithmic Combinatorics

Algorithmic Combinatorics at RISC is devoted to research that combines computer algebra with enumerative combinatorics and related fields like symbolic integration and summation, number theory (partitions, q-series, etc.), and special functions.

Symbolic Methods in Kinematics

Designing mechanical devices, called linkages, that perform a prescribed motion has been a topic that interested engineers and mathematicians for hundreds of years. We apply techniques from algebraic geometry and symbolic computation to various problems in this area, for example the classification of closed 6R linkages, the study of pentapods and hexapods, or the construction of planar linkages. In this context, the concept of motion polynomial and the theory of bonds have been developed, which are powerful tools to answer questions arising in kinematics.

Mathematical Assistant Software (Theorema)

The Theorema project aims at extending current computer algebra systems by facilities for supporting mathematical proving. The present early-prototype version of the Theorema software system is implemented in Mathematica. The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. The individual provers imitate the proof style of human mathematicians and produce human-readable proofs in natural language.

Creating Formal Mathematical Knowledge Bases in Theorema

We create structured mathematical knowledge bases, i.e. digital libraries of theories from all areas of mathematics (set theory, topology, algebra, analysis, probability theory, ...). These knowledge bases are represented in the formal language of Theorema, and the correctness of their contents is established using the automated reasoning capabilities of the system. All this results in a growing collection of fully formal and computer-verified pieces of mathematics that may serve as the foundation of further theory explorations in Theorema.

Formal Methods

By formal methods we understand the application of methods from symbolic computation (especially logic) to reasoning about properties of computer programs, especially about their correctness with respect to a formal specification.

---

Graduate Studies Coordinator