At RISC we are devoted to the foundations, the design, and the implementation of software to generate mathematical proofs. The main enterprise in the area of automated reasoning at RISC is the Theorema project. Theorema has been initiated around 1995 ...
RISC Research Topics
More
The Computer Algebra and Applications (CAA) Group at RISC develops computer algebra algorithms and implements mathematical software packages with the emphasis to apply them to non-trivial applications. ...
Algebraic differential equations can be treated by symbolic geometric methods. Parametrization of algebraic varieties leads to solutions of the corresponding differential equation. ...
Computer Algebra for Geometry Algebraic varieties are defined by polynomial equations. Computer algebra methods for solving systems of polynomial equations and similar problems form the basis for a computational theory of Algebraic Geometry. From the preface of J. R. Sendra, ...
At RISC we understand by formal methods the application of methods from symbolic computation (especially from formal logic) to rigorously reason about properties of computer programs, in particular to verify their correctness with respect to a specification. ...
Rewriting-related Techniques and Applications We investigate solving methods for equational and membership constraints, generalization techniques in various theories, and calculi for conditional rule-based transformations. The developed algorithms and procedures are useful for equational reasoning, program analysis, and declarative programming. Our ...
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 ...