The RISC Curriculum in Symbolic Computation
RISC Courses
RISC offers three kinds of courses:
- Curriculum Courses
- These are the core courses of the
curriculum; every Ph.D. student performs course work in the amount of at least
30 ECTS points. The curriculum courses are offered annually or biennially;
additionally Special Topics courses with varying content may be
offered.
- Seminars
- In seminars, the RISC faculty discusses the state of the art in
research and ongoing project work. In the first year, every Ph.D. student
attends (as a listener) several seminars; later the student attends (as an
active participant) at least one seminar per semester. Seminar topics vary from
semester to semester, the ones listed below are just examples.
- Standard Courses
-
These are courses offered by RISC for
bachelor/master students in mathematics or computer science. They are actually
not part of the RISC curriculum but they may help in exceptional cases to
supplement the education of new Ph.D. students.
According to the general working areas of RISC, the courses are structured into
three categories. Short course descriptions are given in the appendix.
Computer Algebra
Curriculum Courses
Seminars (Examples)
- Seminar "Computer Algebra"
- Seminar "Algorithmic Algebra"
- Seminar "Algorithmic Combinatorics
- Seminar "Algebraic Geometry"
- Seminar "Symbolic Summation for Particle Physics"
- Seminar "Symbolic Summation and Special Functions"
- Seminar "Fundamentals of Numerical Analysis and Symbolic Computation"
Standard Courses
- Algebra
- Analysis
- Linear Algebra 1 and 2
- Linear Algebra for Physicists 1 and 2
- Linear Algebra and Analytic Combinatorics 1 and 2
- Linear Algebra and Analytic Geometry 1 and 2
- Ordinary Differential Equations and Dynamical Systems 1
- Algebraic and Discrete Methods for Biology
- Preparatory Course Mathematics for Beginners of Business Informatics
Computational Logic
Curriculum Courses
Seminars (Examples)
- Seminar "Automated Reasoning (Theorema)"
- Seminar "Set Theory and Logical Foundations"
- Seminar "Formal Methods"
Standard Courses
- Logic as a Working Language
- Logic for Computer Science
- Mathematics and Logic
- Computability and Complexity
- Formal Foundations in Business Informatics
Mathematical Software
Curriculum Courses
Seminars (Examples)
- Bachelor Seminar "Selected Algorithms in Symbolic Computation"
Standard Courses
- Practical Software Technology
- Software Engineering
- Project Engineering
- Algorithms and Data Structures
- Information Systems
- Computer Systems
- Algorithmic Methods 1
Course Descriptions
In the following, we give short descriptions of the courses of the RISC
curriculum.
Computer Algebra
- Computer Algebra: ECTS 4.5, annually.
-
A theoretical introduction to the area of computer algebra is presented.
The list of topics includes basic algebraic domains, greatest common
divisors of polynomials, the Chinese remainder algorithm, factorization
of polynomials, and the theory of Gröbner bases.
- Gröbner Bases: ECTS 3, biennially.
-
The algorithmic theory of Gröbner bases is one of the outstanding tools in
mathematics that enables one to tackle "in principal a huge class of
problems arising in sciences, in particular in mathematics and computer
sciences. In this lecture the underlying concepts are worked out and
Buchberger's distinguished algorithm and their optimized variants are discussed.
Special emphasis is put on applications, in particular, on how non-trivial
problems of sciences can be formulated into the setting of Gröbner basis
theory and on how they can be attacked with the available algorithms.
- Fast Arithmetic and Factorization: ECTS 3, biennially.
-
How many field operations are needed to multiply two univariate polynomials of
degree n over some field K? How about the number of field operations needed for
factoring a polynomial or computing a greatest common divisor of two
polynomials? Efficient algorithms for these and other problems were presented in
Computer Algebra I, but are they as efficient as can be? It turns out that they
are not. In Computer Algebra II we will present faster algorithms, including
some of the fastest algorithms known today for solving algebraic problems
- Elimination Theory: ECTS 3, biennially.
-
This course is concerned with algorithmic approaches to the solution
of polynomial equations. Typical approaches include resultants,
Gröbner bases and characteristic sets.
- Commutative Algebra and Algebraic Geometry: ECTS 7.5,
biennially.
-
In this course the relation between the algebraic theory of polynomial ideals
and the geometry of curves, surfaces, and algebraic varieties is described.
Topics include Hilbert's basis theorem, Hilbert's Nullstellensatz,
polynomial and rational functions on varieties, singular points,
parametrizations, and determination of dimension.
- Algorithmic Algebraic Geometry: ECTS 3, biennially.
-
Algebraic Geometry aims at the understanding of the structure of algebraic
varieties, which are defined as the solution sets of algebraic equation
systems. As this branch of mathematics has a long and rich history, the
amount of available theorems is enormous. In Algorithmic AG, we have a look
at some of these results from the constructive point of view: instead of
being content with the mere existence of some structure (like singularity
resolution, special divisors, fibrations), we want to compute it
effectively.
- Computer Analysis: ECTS 3, biennially.
-
Symbolic methods for integration and the analysis and solution of
differential equations are described.
- Symbolic Linear Algebra: ECTS 3, biennially.
-
In many applications of symbolic computation (e.g., summation,
integration, solving difference/differential equations) one has to
solve systems of linear equations that are not defined over
floating-point numbers, but for instance over rational function
fields or over principle ideal domains. In this lecture we discuss
how to generalize and/or optimize the well-known linear algebra
methods in order to solve such systems. The application of these
methods are illustrated by various examples.
- Computer Algebra for Concrete Mathematics: ECTS 4.5, annually.
-
The major topics of this course include sums, recurrences,
elementary number theory, binomial coefficients, generating functions,
and asymptotic methods. The emphasis is on manipulative
technique rather than on existence theorems or combinatorial reasoning.
Theoretical exposition will be supplemented by computer algebra methods
like Zeilberger's algorithm. (Literature: "Concrete Mathematics -
A Foundation for Computer Science by R.L. Graham, D.E. Knuth
und O. Patashnik, and other books and papers.)
- Algorithmic Combinatorics: ECTS 4.5, annually.
-
The course provides an introduction to enumerative
combinatorics. Topics are: special sequences like
Stirling numbers, partition theory, and important
general concepts like group actions and Polya's
counting theory. Theoretical exposition
will be supplemented by computer algebra methods.
- Symbolic Summation and
Special Functions 1: ECTS 3, biennially.
-
Some functions from
analysis arise so often in applications that we give them special names. Paul
Turan once remarked that such special functions would be more appropriately
labeled "useful functions. Beginning with Newton and Leibniz, special
functions have been continuously developed, including significant
contributions by Euler, Legendre, Laplace, Gauss, Kummer, Eisenstein, and
Riemann. In recent years the interest in special functions has been renewed,
also due to new computer algebra applications. The lecture introduces to
fundamental themes like gamma function, hypergeometric series, and Bessel
functions. Theoretical exposition will be supplemented by computer algebra
methods. (Literature: "Special Functions by G.E. Andrews, R. Askey, and
R. Roy.)
The lecture introduces also the theoretical foundations of symbolic summation:
greatest factorial factorization (GFF) in connection with indefinite summation
of rational and hypergeometric sequences. As applications, famous algorithms
as those of Gosper and Zeilberger are discussed.
- Symbolic Summation and Special Functions 2: ECTS 3, biennially.
-
The course is designed in such a way that it can be followed
independently from having attended "Special Functions 1. Topics
include: orthogonal polynomials (e.g., Chebyshev, Hermite, Laguerre,
Jacobi) and related themes like the irrationality of the Riemann
zeta function at z=3; in addition, an introduction to q-series
is provided. As in Part I, theoretical exposition
will be supplemented by computer algebra methods.
(Literature: "Special Functions by G.E. Andrews,
R. Askey, and R. Roy.)
Based on works by Karr, the lecture also presents a difference field approach to
symbolic summation. It can be seen as a discrete analogon to Risch integration
theory. Due to work of Schneider, various extensions of Karr's theory have
become a powerful tool which can be used in highly nontrivial applications in
special functions, combinatorics, physics, etc.
- Category Theory for Symbolic Computation: ECTS 3, biennially.
-
Directional structures between two objects occur widely in mathematics and
computer science. Category theory emerged as a frame for formalizing such
arrow concepts. Its capacious applicability originates from describing
structure in terms of the existence of arrows and relations between them
rather than intrinsic properties of objects. Categories themselves arise as
abstraction of essentially algebraic theories. Besides its non-constructive
parts category theory is concerned with concepts which are mainly algorithmic
in nature. In this course we concentrate on this particular aspect of the
theory.
- Algebraic Methods in Kinematics: ECTS 3, biennially.
-
In kinematics, the motions of rigid bodies are described by concepts like
position, orientation, velocity etc. These concepts are related to the group of
Euclidean displacements. This group and the class of functions into it
describing motions can be described efficiently and investigated by means of
quaternions, Lie groups, or algebraic geometry. These descriptions will be
explained and applied to typical problems in kinematics, such as the
construction of linkages generating a prescribed motion, or the classification
of overconstrained linkages.
- Algebraic Topology: ECTS 3, biennially.
-
The course gives an introduction to algebraic topology. After developing the
central concepts of homotopy theory we discuss several homology theories. Then
the relations between these approaches are considered. The necessary categorical
language will be explained on demand.
- Homological Algebra: ECTS 3, biennially.
-
Since their emergence in algebraic topology, homological concepts have proved
their efficiency in several mathematical disciplines. Homological algebra is the
theory of these concepts formulated in an abstract categorical setting. After
introducing the basic categories of chain complexes and their homotopy
categories we proceed towards derived functors on abelian categories. The final
lectures are devoted to the development of spectral sequences.
- Special Topics in Computer Algebra: ECTS 3, on demand.
Computational Logic
- Thinking, Speaking, Writing 1+2: ECTS 6, annually.
- TSW 1: Understanding and creating mathematical proofs.
RISC is one of the few institutes in the world offering the lecture
"Thinking, Speaking, Writing, whose purpose is to train the student in
all activities involved in scientific work.
The first part of the course consists in training in formal reasoning:
understanding formal mathematical texts, formalizing mathematical notions,
and especially working with formal mathematical texts (proving).
As we consider the ability to develop correct proofs as being at the very
core of the activity in computer mathematics, the lecture consists in
intensive training in basic proof techniques and in-depth understanding
and mastering of formal mathematics.
- TSW 2: Communication of scientific results.
-
The career of a scientist relies heavily of his ability to communicate
his results through scientific publications and conference talks.
The second part of TSW teaches the basic principles and trains the
abilities necessary to communication of scientific results in an effective
and efficient manner. The subjects include: presentation of scientific
results in oral and written form, working with the scientific literature,
attending scientific presentations, and cooperating in research groups.
- Mathematical Logic: ECTS 7.5, annually.
-
The course is an introduction to logic for students in Computer Science
and Mathematics.
The purpose of the course is to understand the principles of Mathematical
Logic and its mathematical models, and to acquire the skills for using it
in Mathematics and Computer Science.
The course covers the main models: propositional logic, first-order
predicate logic, higher-order logic, as well as the main proof systems for
these models.
Furthermore the lecture demonstrates and trains the practical use of
Mathematical Logic in Mathematics (building theories, proving), and in
Computer Science (automatic reasoning, programming, describing and proving
properties of programs).
- Topics in Mathematical Logic: ECTS 3, biannually.
-
In this course some deeper results in the area of predicate logic are presented,
like Gödel's completeness theorem, omitting types theorem, Craig's
interpolation theorem, Gödel's incompleteness theorem, as well as applications
of elementary chains and ultraproducts.
- Automated Reasoning: ECTS 3, biennially.
-
Introduction to Automated Reasoning: This course presents and compares the basic
methods for Automated Reasoning: the resolution method and the main methods for
proving in natural style. The topics of the lecture are: syntax and semantics of
logical formulae, normalization of formulae, the Herbrand Theorem, the proof
method by resolution, the sequent calculus and its use in automated reasoning,
basic methods for reasoning with equality. Some concrete implementations will be
also presented, including the implementation in Theorema of natural style
proving, as well as some applications of automated reasoning in Mathematics and
Computer Science.
- Advanced Automated Reasoning: ECTS 3, biennially.
-
Advanced Topics in Automated Reasoning: This course presents and compares some
advanced methods for automated reasoning: refinements of the resolution method,
the use of paramodulation for theories with equality, search strategies in
natural style proving, the use of meta-variables in sequent calculus, natural
deduction for theories with equality and the Knuth-Bendix completion method,
methods for combining general and domain specific reasoning, logic-based
algorithm synthesis. The course will also present some practical implementations
of these methods, including natural deduction in the Theorema system, as well as
current applications of automated reasoning in Mathematics and Computer Science.
- Computability Theory: ECTS 3, biennially.
-
This course deals not with algorithms for specific problems, but with the notion
of computability itself. This means that the class of algorithmically computable
(partial recursive) functions is investigated mathematically. Among other things
it is shown that certain problems are algorithmically undecidable, that is, they
cannot be solved by computer programs even in principle.
- Decidability and Complexity Classes: ECTS 3, biennially.
-
The first part of this course is a sequel to Computability Theory.
Algorithmically undecidable problems may be reduced to each other and thus
compared with respect to the degree of undecidability. The second part deals
with various aspects of abstract complexity theory, including NP-completeness.
- Decidable Logical Theories: ECTS 3, biennially.
-
In this course decision algorithms are given for various logical theories,
specifically, for the set of all true sentences in some model or the set of all
consequences of some set of axioms. Some examples are Presburger arithmetic, and
the theories of real closed fields, Abelian groups and linear orderings. Various
basic methods for developing such decision algorithms are introduced, the most
important being quantifier elimination.
- Rewriting in Computer Science and Logic: ECTS 3, biennially.
-
Equational theories appear in many areas of mathematics, logic, and computer
science. Methods for turning a set of equational axioms into an equivalent set
of rewrite rules are discussed. The Knuth-Bendix procedure and the Gröbner
basis algorithm are typical examples of such transformations.
- Unification theory: ECTS 3, biennially.
-
Unification, or equation solving in abstract algebras, has been studied since
the beginning of mathematics. It is concerned with the problem of identifying
given terms, either syntactically or modulo a given theory. Unification is at
the very heart of computation in a given logic: It is the basic operation in
automated reasoning, rewriting, completion, logic programming, and in the
related areas. This course presents first-order syntactic and equational
unification, and higher-order unification and matching.
- Gödel's Incompleteness Theorems: ECTS 3, biennially.
-
Gödel's incompleteness theorems are two theorems of mathematical logic
that establish inherent limitations of all but the most trivial axiomatic
systems for mathematics. The theorems, proven by Kurt Gödel in 1931, are
important both in mathematical logic and in the philosophy of mathematics.
The two results are widely interpreted as showing that Hilbert's program
to find a complete and consistent set of axioms for all of mathematics is
impossible, thus giving a negative answer to Hilbert's second problem.
The first incompleteness theorem states that no consistent system of
axioms whose theorems can be listed by an "effective procedure"
(essentially, a computer program) is capable of proving all facts about
the natural numbers. For any such system, there will always be statements
about the natural numbers that are true, but that are unprovable within
the system. The second incompleteness theorem shows that if such a system
is also capable of proving certain basic facts about the natural numbers,
then one particular arithmetic truth the system cannot prove is the
consistency of the system itself.
This course is intended for students of mathematics or computer science
who are interested on the theoretical foundations of computer science.
There is no particular prerequisite for the course.
- Formal Methods in Software Development: ECTS 6, annually.
-
This course gives a survey on the theory and practice of formal methods in the
development of sequential and concurrent software, as they are more and more
used in industrial practice for ensuring the correctness of critical system
components. Introducing the logical foundations of of Hoare Calculus, predicate
transformers, and programs as relations on system states, we will investigate
various tools for program specification (e.g. the Java Modeling Language JML),
extended static checking (e.g. Esc/Java2), model checking (e.g. the model
checker SPIN), and program verification by computer-supported proving (e.g. the
RISC ProgramExplorer).
- Formal Semantics of Programming Languages: ETCS 3,
biennially.
-
This course describes various approaches to define the meaning of a programming
language in a mathematically precise way and to reason on this basis about the
constructs of the language. These approaches are denotational semantics
(programs as functions on semantic domains), operational semantics (programs as
state transitions), and axiomatic semantics (programs described by
pre/post-condition pairs). We investigate their core ideas, their domain of
applicability, and their relationship.
- Formal Specification of Abstract Datatypes: ECTS 3, biennially.
-
This course describes the axiomatic/algebraic approach of specifying abstract
datatypes (respectively "classes in object-oriented terminology) in a
mathematically precise way. We will introduce the core theory, investigate
various application examples, and demonstrate languages and software systems
(e.g. CafeOBJ and CASL) for writing, checking, and even executing such
specifications.
- Formal Models of Parallel and Distributed Systems: ECTS 3,
biennially.
-
Concurrent and reactive computing systems are difficult to grasp, because they
generally exhibit in different runs different behaviors, due to the
time-dependent interleaving of operations from different processes. For an
adequate understanding of such systems, formal models are of crucial importance.
This course introduces two fundamental approaches to specify the behavior and to
reason about the properties of such systems, one based on temporal logic (as
exemplified by the Temporal Logic of Actions TLA) and one based on process
calculus/algebra (as exemplified by CCS and the pi-Calculus).
- Formal Languages and Formal Grammars 1: ECTS 3, biennially.
-
In this course we introduce and study the basic abstract models of
computation, namely finite state machines, push down machines, and formal
grammars, and their relationships to formal languages. It is also
discussed how the abstract computing devices are used to process
languages, and hence to solve problems that are of practical relevance.
The notion of a formal grammar arises from the need to formalize the
informal notions of grammar and language. Many formal grammars were
invented and they can be ordered in a natural hierarchy.
There are no special prerequisites in terms of specific courses to attend.
Students are expected to be familiar with the basic notions of mathematics
and with basic proof techniques, as taught in the mathematics courses of
the first year.
- Formal Languages and Formal Grammars 2: ECTS 3, biennially.
-
Within the first part of the course, we introduced some of the basic
notions, e.g, finite state machines, push down machines, and formal
grammars, and their relationships to formal languages. Within this part we
will introduce the Turing Machine in various ways and see that all of them
turn to be equivalent. While the first part of the course was dedicated to
the theoretical apparatus needed for contracting syntactically correct
programs, the second part will introduce the semantical meaning of a
program. In particular, we will introduce a mapping between program texts
and computable functions.
There are no special prerequisites in terms of specific courses to attend.
Students who have not attended the first part of the course may also
attend this part -- when necessary, we will have some additional exercises
in order to fill gaps. Students are expected to be familiar with the basic
notions of mathematics and with basic proof techniques, as taught in the
mathematics courses of the first year.
- Fixpoint Theory of Functional Programs: ECTS 3, biennially.
-
In this course we study the fixpoint theory of programs, developed by D.
Scott, and we consider the semantics of programs defined as least
fixpoints of recursive operators. The topics we will cover include:
Computable, partial, total and recursive functions; Decidable and
semidecidable sets. The halting problem; Compact, continuous, effective
and recursive operators; Knaster-Tarski, Myhill-Shepherdson and Kleene
theorems; Fixpoint induction, Scott induction rule for proving properties
of programs.
This course is intended for students of mathematics or computer science
who are interested on the theoretical foundations of computer science.
There is no particular prerequisite for the course.
- Special Topics in Computational Logic: ECTS 3, on demand.
-
Mathematical Software
- Programming Project Symbolic Computation 1+2: ECTS 6, annually.
-
In this programming project, the overall process of the team-oriented
development of non-trivial mathematical software using modern development
tools is exercised.
- Design and Analysis of Algorithms: ECTS 3, biennially.
-
In this course algorithms are presented for specific problems in various areas
of mathematics like sorting, graph theory, pattern matching and arithmetic. It
also includes the discussion of general principles of algorithm design like
`Divide and Conquer' or dynamic programming, as well as techniques for analyzing
the complexity of algorithms.
- Introduction to Parallel and Distributed Computing: ECTS 3,
biennially.
-
This course gives an introduction to programming parallel and distributed
computer systems. We give an overview on parallel computer architectures,
discuss the principles of engineering parallel software, and program simple
examples in various programming models, e.g. SPMD (single program, multiple
data) programming with automatically parallelizing compilers and message passing
programming in the MPI (message programming interface) standard.
- Logic Programming: ECTS 3, annually.
-
Logic programming paradigm has its roots in deduction, and combines it
with the computation of values. This course gives an introduction to
logic programming, mainly through the Prolog programming language.
- Functional Programming: ECTS 3, annually.
-
The course is an introduction to functional programming and to the Lisp
programming language. The course covers the basic principles of functional
programming (recursive definition of data structures and program construction
using recursion, tail-recursion and its relation to iterative programs), as well
as the main constructs of the Lisp language (constructing and accessing lists,
conditional and iterative programming constructs, use of Lisp for symbolic
computation).
- Programming in Mathematica: ECTS 3, annually.
-
This course illustrates the programming language of the well-known symbolic
computation system Mathematica. The course is targeted towards students with a
strong mathematical background and the exercises always have a mathematical
flavor. We concentrate on features of the language, which make programming in
Mathematica different from standard procedural programming as taught in the
introductory programming courses for students of Mathematics, thus we emphasize
pattern matching, rule-based programming style, functional programming style,
and graphics programming
- Chess Programming: ECTS 3, biennially.
-
In the theoretical part varous tasks are considered which can be done
by a computer: playing chess, analyzing and assessing positions,
solving chess problems and creating endgame tablebases. The principles
involved are partially valid for other games as well. Algorithms are
described in an abstract fashion. In the practical part a simple
chess-playing program is developed.
- Computer Algebra Systems: ECTS 3, biennially.
-
Computer algebra systems are nowadays routinely used in mathematics, science,
and engineering for elaborating and solving problems involving symbolic
calculations, such as the exact solution of polynomial equations, of indefinite
integrals, of sums and recurrences, and much more. Prominent examples of such
software are the commercial systems Maple and Mathematica and the open source
systems Axiom, GAP, and Maxima. This course trains the practical use of such
systems by a number of application examples.
- Automated Reasoning Systems: ECTS 3, biennially.
-
Today there exist a number of tools that support formal reasoning in mathematics
and computer science, from simple proof checkers to interactive proof
assistants, fully automatic decision procedures, and comprehensive theorem
proving systems. Examples of such systems are Isabelle/HOL, Coq, ACL2, PVS, and
last but not least the Theorema system developed at RISC. This course trains the
practical use of such systems by a number of application examples.
- Computer-based Working Environments: ECTS 1.5, annually.
-
The GNU/Linux operating system gets nowadays more attention based on
its excellent features in security and privacy. Many free and
open-source programs are available under GNU/Linux.
This course teaches how to get things done in a GNU/Linux system. The
course covers topics such as working with desktop environment and
working on the command line, including a short introduction to commonly
used programs, remote connections, mailing, version control, HTML,
OpenPGP, image processing.
- Special Topics in Mathematical Software: ECTS 3, on demand.
Graduate Studies Coordinator