"A Heuristic Prover for Elementary Analysis in Theorema"
, Serie RISC Report Series, Johannes Kepler University Linz, Austria, Nummer 21-07, RISC, JKU, Hagenberg, Linz, 4-2021
A Heuristic Prover for Elementary Analysis in Theorema
Sprache des Titels:
We present the application of certain heuristic techniques for the automation of proofs in elementary analysis. the techniques used are: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the [Epsilon]-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admisibility of solutions to the metavariables. The proofs are very similar to those produced automatically, but they are edited for readability and aspect, and also for inserting the appropriate explanation about the use of the proof techniques. The proofs are: convergence of product of two sequences, continuity of the sum of two functions, uniform continuity of the sum of two functions, uniform continuity of the product of two functions, and continuity of the composition of functions.
Sprache der Kurzfassung:
RISC Report Series, Johannes Kepler University Linz, Austria