@**techreport**{RISC3848,author = {Vajda Robert},

title = {{Supporting Exploration in Elementary Analysis by Computational, Graphical and Reasoning Tools}},

language = {english},

abstract = {The present thesis investigates the requirements for a computer supported learning environment for elementary analysis and it contributes to the development of such an environment.
An ideal environment would be able to provide computer support for any phases of the mathematical
exploration. It turns out that existing known mathematical assistant systems, like general-purpose computer algebra systems provide efficient and user-friendly graphical and computational tools for the phase of experimentation and application. So, they should be just adjusted to the specials needs of a particular mathematical field like analysis.
However, the essential part of mathematics, i.e. reasoning, is rarely covered yet by assistant systems.
Therefore, in the focus of this thesis is the computer support for proving problems occurring in elementary analysis. The main contribution of the author is the extension of the combined techniques for proving standard theorems in elementary analysis: the combined methods link logical and algebraic techniques.
The algebraic techniques provide instantiations on existentially quantified variables in the goal formula, when finding appropriate witnesses for the existentially quantified variables within a purely logical calculus
is difficult and inefficient.
Based on PCS-method and the S-Decomposition strategy and exploiting the method of quantifier elimination, reasoners for elementary analysis are designed and implemented in the Theorema proving system. Several deduction examples are provided by the author in the case studies for elementary analysis, putting an emphasis also on didactical issues during the exposition.},

number = {09-11},

year = {2009},

month = {June},

annote = {PhD Thesis},

keywords = {computer supported learning environment, computer algebra, automated reasoning, elementary analysis, quantifier elimination, Mathematica, Theorema},

length = {98},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}