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 (www.theorema.org), provides a uniform logic frame for the exploration of mathematical theories [1], 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 [4] - 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 [5, 3] - 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 [2] 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.
| [1] | B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa, F. Piroi, N. Popov, J. Robu, M. Rosenkranz, and W. Windsteiger. Theorema: Towards Computer-Aided Mathematical Theory Exploration. Journal of Applied Logic, 2005. | |
| [2] | T. Jebelean. Natural Proofs in Elementary Analysis by S-Decomposition. RISC Report 01-33, November 2001. | |
| [3] | T. Jebelean. Using Computer Algebra for Automated Reasoning in the Theorema System, 2005. Invited talk at Seventh Asian Symposium on Computer Mathematics (ASCM 2005). | |
| [4] | L. Kovacs and T. Jebelean. Finding Polynomial Invariants for Imperative Loops in the Theorema System. In S. Autexier and H. Mantel, editors, Proceedings of Verify 06 Workshop, IJCAR 06, The 2006 Federated Logic Conference, pages 52-67, 2006. | |
| [5] | R. Vajda, T. Jebelean, and B. Buchberger. Combining Logical and Algebraic Techniques for Natural Style Proving in Elementary Analysis. Mathematics and Computers in Simulation, 2008 (in print). |
Contact Tudor at:
Prof. Dr. Tudor Jebelean
Research Institute for Symbolic Computation (RISC)
Johannes Kepler University of Linz
A-4040 Linz, Austria
Tudor.Jebelean at risc.uni-linz.ac.at
http://www.risc.uni-linz.ac.at/home/tjebelea/