Abstract: We present some applications of the Theorema system to the generation of invariants for imperative loops and to automated proving in elementary analysis, which are based on the interaction of logic
techniques with methods from computer algebra and from algebraic combinatorics. The Theorema project (<link www.theorema.org>www.theorema.org</link>), provides a uniform logic frame for the exploration of mathematical theories, based on automatic reasoning. The use of combinatorial and algebraic methods in conjunction with automated reasoning leads to powerful analysis tools, because they allow the automatic generation of inductive assertions for programs joint work with Laura Kovacs.

The method generates all the invariants which can be represented as polynomial equations (in fact, a basis for the ideal generated by the corresponding polynomials) in two stages: first the recursive
equations corresponding to the evolution of loop variables are transformed into closed formulae (depending on the loop counter) using combinatorial techniques; second these closed forms are used in
successive applications of the Buchberger algorithm in order to find out the invariant ideal.

We also show how to significantly enhance thepower of automatic provers joint work with Bruno Buchberger and Robert Vajda in particular for reasoning in numeric domains (reals, integers) by using the CAD method (Cylindrical Algebraic Decomposition) in order to generate natural proofs in elementary analysis (the so called epsilon delta proofs). Namely, by applying the S-Decomposition logical technique we decompose the original proof problem into several numerical conjectures which involve existential quantifiers, whose witnesses are then found by CAD. This combination of techniques builds a prover with the distinctive feature that it does not need all the axioms of the underlying domain (e.g. the reals), but it automatically finds the appropriate lemmata which are necessary for completing the
proof.


Biography:
Tudor Jebelean is an Associate Professor in the Theorema group (leader: Bruno Buchberger and Tudor Jebelean) at the Research Institute for Symbolic Computation (RISC), Johannes Kepler University
of Linz, Austria. His main research interests are automated reasoning and program verification using logic and algebraic methods. He holds a PhD in Computer Science and Habilitation title from Johannes Kepler University of Linz.  (<link service.zid.tuwien.ac.at/ts/goto.php _blank>http://www.risc.uni-linz.ac.at/home/tjebelea)</link>