Theorema is a logic and software system developed by the speaker and his research group at RISC (Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria). Its purpose is the integration of formal proving, solving, and computing in one system for doing both formal mathematics and formal software development in an integrated frame. After a short introduction on the philosophy, structure, and main components of the Theorema system, the emphasis of the talk will be on a new method, introduced by the speaker, for the automated synthesis of algorithms from formal problem specifications. The method is called "lazy thinking" because it postpones all creative steps in the synthesis process until the last moment in which the necessary steps are almost stringent from the current synthesis context and, hence, can be automatically generated by (advanced) automated reasoning. The synthesis method will first be illustrated in a simple example. Then, we will show that intellectually quite challenging problems, like the construction of Groebner bases in computer algebra (with lots of applications in such diverse fields like cryptography, systems theory, CAD, robotics etc.), can be tackled by the method. Finally, we will give some outlook on the future of formal mathematics and formal software development and web-based knowledge management.

We present a Maple package for manipulating first-order formulas over the reals. The package, named SyNRAC, provides a set of commands for manipulating real algebraic constraints, aimed at helping resolve various problems derived from application areas such as engineering, bioinformatics and mathematical biology We also show how the package is applied to a practical problem.

Cylindrical algebraic decomposition (CAD) is a general-purpose symbolic method aiming for quantifier elimination (QE) which is a powerful tool to resolve non-convex and parametric optimization problems exactly. However, QE based on CAD is not practical since CAD usually consists of many of purely symbolic computations and has high computational complexity in nature. Therefore, it is strongly desired to develop an efficient algorithm to realize CAD. We propose an effective symbolic-numeric algorithm that uses interval arithmetic and the ``dynamic evaluation" technique in handling algebraic numbers in CAD construction. In this talk we report our implementation on Maple (as a part of SyNRAC) and demonstrate the effectiveness of our approach with numerical examples.

Hybrid systems consist of continuous dynamical systems such as differential/difference equations and discrete dynamical systems such as if-then rules and finite automata. As is well known, hybrid systems represent a broad class of dynamical systems. However, there are few practical applications. One of the reasons is in the practical issues on the computation time to solving the finite-time optimal control problem of hybrid systems. In many cases, the optimal control problem is applied to the model predictive control (MPC) problem, which is one of the standard control methods. In the MPC problem, the optimal control problem must be solved at each discrete time. However, the optimal control problem is in general reduced to a mixed integer quadratic programming (MIQP) problem. Then the computation time to solve the MIQP problem is too long for practical plants. Therefore, practical applications are limited greatly. For overcoming this technical issue, we focus on the modeling of discrete dynamics, and have proposed several techniques such that the branch and bound method works effectively. In this talk, first, the MPC problem of hybrid systems is explained briefly. Next, the previously proposed methods to express discrete dynamics are explained, and the effectiveness of these methods is shown by numerical examples. Finally, based on these methods, the approximate algorithm to solve the optimal control problem is proposed. The key idea of this algorithm is to limit candidates of mode sequences. So the further reduction of the computation time is achieved. On the other hand, it is desirable that many data, which are used effectively for solving the MIQP problem, are calculated in pre-computation (off-line computation). Then it is one of significant works to apply symbolic computation techniques.

In this talk we review the recent development of algebraic approaches that utilize the Sum of Roots (SoR) and see how the SoR effectively relates practical problems in the control field and some algebraic techniques. We first see how the SoR was introduced in the context of control theory. It is then observed that the SoR reveals an intriguing and useful relationship between Groebner basis theory and polynomial spectral factorization, an important mathematical tool in signal processing and control theory. This relationship allows us to devise an algebraic approach for variable elimination. We further discuss that the SoR possesses a nice property that can be exploited when formulating a control problem into a QE problem. Potential directions of development are also mentioned for discussions.

For polynomial spectral factorization, an important mathematical tool in signal processing and control, an algebraic approach is proposed by Kanno et. al. that enables us to carry out parametric polynomial spectral factorization (PPSF). In this talk, we investigate the efficiency of PPSF by means of comprehensive Groebner systems (CGS). More specifically, three methods are devised and their computabilities are compared. A discussion on which approach is most suited to PPSF is provided, and furthermore remarks are given on how improvements of CGS computation can be made for solving general practical problems.

We present a formal approach to verify functions of VLSI circuits using symbolic computer algebra. Our method describes arithmetic circuits in VLSI datapaths directly with high-level mathematical objects based on weighted number systems and arithmetic formulae. Such circuit description can be effectively verified by polynomial reduction techniques using Groebner bases. In this presentation, we describe how the symbolic computer algebra can be used to describe and verify arithmetic circuits. The advantageous effects of the proposed approach are demonstrated through experimental verification of some arithmetic circuits such as multipliers. The result shows that the proposed approach has a definite possibility of verifying practical arithmetic circuits where the conventional techniques failed.

(joint work with Naofumi Homma, Takafumi Aoki, and Tatsuo Higuchi)

Facilities for reasoning about real polynomial inequalities are becoming more widely available and more powerful. However, they are not particularly well-suited to use as an external library or server accessed by another piece of software. This talk will describe some of the challenges facing the designer of an API or protocol for communication between clients and server software that can reason about real polynomial inequalities. In keeping with the aims of this session, this talk will, hopefully, help stimulate and guide a discussion about what such an API or protocol would look like. In particular, how does one meet the needs of users while working within the constraints inherent to reasoning about real polynomial inequalities.

We present a generalization of the Cylindrical Algebraic Decomposition (CAD) algorithm to systems of equations and inequalities polynomial in x, f1(x), ..., fm(x) and y1, ..., yn. f1(x), ..., fm(x) are real univariate functions such that there exists a real root isolation algorithm for functions from the algebra Q[x, f1(x), ..., fm(x)]. In particular, the algorithm applies when f1(x), ..., fm(x) are real exp-log functions.

Modified equation of a finite difference scheme (FDS) is computed by first expanding all grid functions in the scheme into Taylor series in all space and time variables and then by eliminating all time derivatives (except the lowest order one) in the resulting equation. The modified equation carries information on numerical properties of the FDS as order of approximation, stability, diffusivity or dispersivity, and thus is often being used during the design adn verification of new FDS. Computation of the modified equation of a simple FDS is quite easy task for any general computer algebra system as it involves only Taylor expansion and repeated substitutions. Some FDS are however quite complex and include sub-steps where general functions as absolute value or rational functions are applied to mesh functions, which requires computing of Taylor series of these general functions applied to Taylor series. Thus computing the modified equation for such FDS is becoming more complicated and naive approach requires unnecessary computing resources (both in memory and computing time) which even for relatively simple FDS overwhelm current machines. To be able to compute the modified equations of complex FDS we have developed the Maple package in which we represent given FDS by a pseudo-code and process each step of the pseudo-code by repeated Taylor expansion to get the final Taylor expansion from which the needed time derivatives are eliminated. One step of a pseudo-code defines a new grid function using previously defined grid functions or original grid functions for which the FDS is formulated. For repeated usage of given grid function construction the pseudo-code can employ user defined functions which are expanded during the pre-processing. Pseudo-code can include symbolic parameters of given FDS. The package is applied to compute modified equations of several complex FDS including e.g. MPDATA scheme for advection or transport equations in 1D, 2D or 3D, or staggered scheme for Lagrangian hydrodynamics in 1D.

Dynamical systems broadly refers to systems that evolve or change over time. Such systems have been modeled using many different formalisms, such as, discrete state transition systems, continuous time dynamical systems, or hybrid systems that combine the two. In the past several years, we have been involved with analyzing models of dynamical systems coming from a variety of domains. In this talk, we report on the deductive engines that were used in the various analysis efforts. Discrete state transition systems were used to model certain biological processes. These models were analyzed using Satisfiability (SAT) solvers, Satisfiability Modulo Theory (SMT) solvers (the linear arithmetic and SAT components), and symbolic model checkers. Hybrid systems were analyzed using two different techniques. Both techniques rely on checking satisfiability of nonlinear polynomial constraints. The checker, however, need not be sound and complete. One technique requires that answers are correct whenever the checker reports satisfiable, whereas the other technique requires that answers are correct whenever the checker reports unsatisfiable. Discrete state transition models of imperative programs were analyzed using static analysis. The deductive components here computed over-approximations of the logical operators, and, or, and existential quantification, for different abstract domains. For instance, when algebraic sets are used as the abstract domain, the required operations are ideal intersection, union, and elimination ideal computation.

Hybrid systems are dynamical systems combining continuous and discrete state and evolution. They are an important formalism for modeling embedded systems that combine a discrete computing device with an environment obeying the continuous laws of physics. Correctness verification of such hybrid systems usually builds upon constraint solving algorithms. The talk will discuss experiences with some constraint solving algorithms in hybrid systems verification and discuss requirements on such algorithms that ensure their usefulness in this context.

Certain applications of bit-level reasoning, including cryptanalysis and arithmetic circuit verification can benefit from using algebraic methods. On the other hand SAT solvers become more and more powerful and usually are much faster, particularly in a more general setting. In this talk we review various ways to combine SAT solving and algebraic methods. We show how Gaussian elimination can be simulated by extended resolution and discuss why polynomial reasoning seems to be more difficult to handle.

This talk is based on joint work with Toni Jussila.

The hierarchical superposition based theorem proving calculus of Bachmair, Ganzinger, and Waldmann enables the hierarchic combination of a theory with full first-order logic. If a clause set of the combination enjoys a sufficient completeness criterion, the calculus is even complete. We define a generalized notion of subsumption for this calculus that extends the well known first-order subsumption rule by an implication condition for the theory part. For the theory of linear arithmetic this implication condition is effectively decidable by a reduction to linear programming problems. A first, rather naive prototype implementation of the resulting superposition calculus modulo linear arithmetic in SPASS is available. It already shows impressive results on practical verification problems. Due to the expressiveness of the combined language it has a high potential for verification tasks in general and also opens a new branch for theoretical research questions.

(joint work with Ernst Althaus and Christoph Weidenbach)

Embedded digital systems have become ubiquitous in everyday life. Many such systems, including many of the safety-critical ones, operate within or comprise tightly coupled networks of both discrete-state and continuous-state components. Hybrid systems are an expressive modelling paradigm for describing such hybrid discrete-continuous behavior. This talk discusses the fully symbolic and direct approach to the reachability problem of hybrid systems. First, we introduce the concept of a hybrid automaton as a formal model for hybrid systems. In order to facilitate a symbolic treatment, we give a translation scheme to encode the transition relation of a given automaton as a potentially non-linear arithmetic constraint formula over the reals and integers and with a complex Boolean structure. To address the reachability problem, we consider the types of formulae which arise from a) bounded model checking to disprove a specified safety property, and from b) full model checking to prove correctness of the system. At the end of the talk, we briefly sketch a probabilistic extension of a hybrid automaton and a symbolic approach to its analysis.

(joint work with Andreas Eggers, Martin Fränzle, Christian Herde, Holger Hermanns, Stefan Ratschan, and Tobias Schubert)

We describe a system for model checking of linear hybrid systems with large discrete state spaces. Our system builds on AND-inverter graphs extended with linear constraints as efficient symbolic representations of hybrid state spaces. It combines Weispfenning-Loos quantifier elimination for the computation of continuous flows and sophisticated SMT-based redundancy detection techniques for maintaining compactness of the data structures.

(joint work with Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, and Boris Wirtz)

Many problems occurring in verification can be reduced to proving the satisfiability of conjunctions of literals in a background theory. This can be a concrete theory (e.g. the theory of real or rational numbers), the extension of a theory with additional functions (free, monotone, or recursively defined) or a combination of theories. It is therefore very important to have efficient procedures for checking the satisfiability of conjunctions of ground literals in such theories. We present some new results on hierarchical and modular reasoning in complex theories, as well as several examples in verification in which efficient reasoning is possible. We will then present the way in which these methods can be used in the context of verification of parametric systems, in order to infer constraints on the parameters which guarantee safety.

(some of the results presented here were obtained in joint work with Carsten Ihlemann and Swen Jacobs)

Real life applications of automated reasoning, like program verification and computer aided education, need to use rich theories for the underlying domains. We present here our experience in computer aided building of some elementary theories, on one hand, and in using sophisticated algebraic methods in the frame of proving, on the other hand: