Institute of Computer Languages
Compilers and Languages Group

Talks 2009 - Tudor Jebelean

The Compilers and Languages Group invites you to a talk given by

Prof. Dr. Tudor Jebelean

RISC-Linz, Johannes Kepler University, Linz, Austria


Combining Automated Reasoning and Algebraic Methods in Theorema

Date: Wednesday, February 4th, 2009
Time: 15:00 (c.t.)
Location: TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte)


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 (, 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 the power 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.

About Prof. Dr. Tudor Jebelean:

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

Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.

   About Us
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)