RISC-Linz RISC-Linz Research Institute for Symbolic Computation  
about
|
people
|
publications
|
research
|
education
|
industry
|
conferences
|
media
|
projects
internal
  
search:
  

The RISC Curriculum in Symbolic Computation

Research Topics

Within the realm of symbolic computation, research at RISC mainly falls into three general categories: Symbolic Computation
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.

CA for Differential Equations
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
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
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.

Theorema
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.

Theorema
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
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