Techniques for Natural-style Proofs in Elementary Analysis

Author: Tudor Jebelean

Paper Information

Title:Techniques for Natural-style Proofs in Elementary Analysis
Authors:Tudor Jebelean
Proceedings:SCSC Papers
Editors: Anna Maria Bigatti and Martin Brain
Keywords:Satisfiability Checking, Natural-style Proofs, Symbolic Computation

ABSTRACT. Combining methods from satisfiability checking with methods from symbolic computation promises to solve challenging problems in various areas of theory and application. We look at the basically equivalent problem of proving statements directly in a non-clausal setting, when additional information on the underlying domain is available in form of specific properties and algorithms. We demonstrate on a concrete example several heuristic techniques for the automation of natural-style proving of statements from elementary analysis. The purpose of this work in progress is to generate proofs similar to those produced by humans, by combining automated reasoning methods with techniques from computer algebra. Our techniques include: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behaviour in zero, bounding the epsilon-bounds, rewriting of expressions involving absolute value, algebraic manipulations, and identification of equal terms under unknown functions. These techniques are being implemented in the Theorema system and are able to construct automatically natural-style proofs for numerous examples including: convergence of sequences, limits and continuity of functions, uniform continuity, and other.

Talk:Jul 11 12:15 (Session 64G: Extended Abstracts: Symbolic Computation)