The RISC Curriculum in Symbolic Computation
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
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 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