Tudor Jebelean,
"A Heuristic Prover for Elementary Analysis in Theorema"
, in F. Kamaredine, C. Sacerdoti Coen: Intelligent Computer Mathematics, 14th International Conference, CICM 2021, Timisoara, Romania, Serie Lecture Notes in Artificial Intelligence (LNAI), Vol. 12833, Springer, Seite(n) 130-134, 7-2021, ISBN: 978-3-030-81096-2
Original Titel:
A Heuristic Prover for Elementary Analysis in Theorema
Sprache des Titels:
Englisch
Original Buchtitel:
Intelligent Computer Mathematics, 14th International Conference, CICM 2021, Timisoara, Romania
Original Kurzfassung:
We present a plug-in to the Theorema system, which generates proofs similar to those produced by humans for theorems in elementary analysis and is based on heuristic techniques combining methods from automated reasoning and computer algebra. The prover is able to construct automatically natural-style proofs for various examples related to convergence of sequences as well as to limits, continuity, and uniform continuity of functions. Additionally to general inference rules for predicate logic, the techniques used are: the S-decomposition method for formulae with alternating quantifiers, use of 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 admissibility of solutions to the metavariables. The problem of proving such theorems directly without using refutation and clausification is logically equivalent to the problem of satisfiability modulo the theory of real numbers, thus these techniques are relevant for SMT solving also.