Combining methods from satis ability 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 speci c 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 quanti ers, quanti er elimination by cylindrical algebraic decomposition, analysis of terms behaviour in zero, bounding the -bounds, rewriting of expressions involving absolute value, algebraic manipulations, and identi cation 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.
The need for natural1{style proofs (that is: similar to proofs produced by humans { see [2]) arises in various applications, as for instance in tutorials, demonstrations, and interactive teaching systems. Some authors argue for the use of natural style when the proof system is not completely automatic (e. g. interactive provers) because this facilitates the interaction with the human user. ? Partially supported by project \Satis ability Checking and Symbolic Computation" (H2020-FETOPN-2015-CSA 712689). 1 Here we do not mean natural deduction as described e. g. in [7].
When applied to problems over reals, Satis ability Modulo Theories (SMT) solving combines techniques from Automated Reasoning and from Computer Algebra. From the point of view of Automated Reasoning, proving unsatis ability of a set of clauses appears to be quite di erent from producing natural-style proofs. Indeed the proof systems are di erent (resolution on clauses2 vs. some version of sequent calculus3), but they are essentially equivalent, relaying on equivalent transformations of formulae. Moreover, the most important steps in rst{order proving, namely the instantiations of universally quanti ed formulae (which in natural{style proofs is also present as the equivalent operation of nding witnesses for existentially quanti ed goals), are actually the same or very similar. (For an illustration of instantiations in natural{style proofs see [4].) From the point of view of Computer Algebra, nding these instantiations is the most important operation, thus here again one can use the same techniques in SMT solving and natural{style proving. Therefore the techniques can be easily moved from one area to the other, because they are essentially equivalent.
In this paper we present our results on a class of proof problems which arise in elementary analysis. These are problems involving formulae with alternating quanti ers, which are di cult to solve by the purely logic approach, because this requires the use of a large number of formulae which express the necessary properties of numbers (naturals, integers, rationals, reals). We use the following techniques, which extend our previous work [8]: { the S-decomposition method for formulae with alternating quanti ers [6], { Quanti er Elimination by Cylindrical Algebraic Decomposition [3], { analysis of terms behaviour in zero, { bounding the -bounds, { rewriting of expressions involving absolute value, { algebraic manipulations: solving, substitution, and simpli cation, { identi cation of equal terms under unknown functions.
Our prover, implemented in the frame of the Theorema system [2], aims at producing natural{style proofs for simple theorems involving limits of sequences and of functions, continuity, uniform continuity, etc. An important aspect of the naturalness of the proof is the fact that the prover does not need to access a large collection of formulae (expressing the properties of the domains involved). Rather, the prover uses symbolic computation techniques from algebra in order to discover relevant terms and to check necessary conditions, and only needs as starting formulae the de nitions of the main notions involved.
The prover can run either in interactive mode (the user has a choice of certain techniques at certain points) or fully automatic mode, because this is provided by the Theorema system. When in automatic mode, the proofs tested by us took at most 30 seconds. 2 en.wikipedia.org/wiki/Resolution (logic) (May 2018) 3 www.encyclopediaofmath.org/index.php/Sequent calculus (May 2018), en.wikipedia.org/wiki/Sequent calculus (May 2018)
Example: Product of Convergent Sequences We illustrate our method by the proof of the theorem \The product of two convergent sequences is convergent.", which is presented in detail on the next pages. The lines labeled [K1], . . . , [K5] are not part of the proof, but only annotations for the purpose of this presentation: they indicate the key steps in the proof where special symbolic methods have to be used.
Note the speci c structure of the quanti ed formulae: the quanti er has a rst underline which declares the type of the variable, and possibly a second underline which declares a condition upon the quanti ed variable. These two conditions have a speci c role during the decomposition of the proof using our method { see [1]. For space reasons, in this presentation we do not address the treatment of types. Note also that we follow the convention of Mathematica and Theorema, by denoting function and predicate application by square brackets instead of the traditional round parantheses.
The proof starts from the de nition of the notion of convergent sequence and
of the product of sequences, and decomposes the theorem into 3 statements: two
assumptions (
The main structure of the proof follows from the S-decomposition method (see [6]): the quanti ers are removed from the 3 statements in parallel, using a combination of inference steps which decompose the proof into several branches, introduce Skolem constants4, and require special terms (for instantiations or as witnesses). In the background the prover keeps certain quanti ed formulae which express the general structure of the proof and which are used at certain moments for nding the witnesses and the instantiation terms (as described in [1]).
At the beginning the 3 formulae are existential, in this situation
S-decomposition is applied as follows:
{ First for the assumptions (
As an e ect of this transformations the 3 formulae become universal (
De nition: The sequence f : N
! R is convergent i : a29R e2R M92Nnn82MNjf [n] aj < e 8 e>0
Proof:
We assume:
(
(
[K5] Algebraic manipulations Using elementary properties of R we transform (16) into: (20) ja1 (f2[n0] a2) + a2 (f1[n0] a1) + (f1[n0] a1) (f2[n0] Using elementary properties of R, from (18) and (19) we obtain: (21) ja1 (f2[n0] a2) + a2 (f1[n0] a1) + (f1[n0] a1) (f2[n0] ja1 (f2[n0] a2)j + ja2 (f1[n0] a1)j + j(f1[n0] a1) (f2[n0] a2)j < e0 a2)j a2)j = = ja1j jf2[n0] a2j + ja2j jf1[n0] a1j + jf1[n0] a1j jf2[n0] a2j < < ja1j e + ja2j e + e e
ja1j e + ja2j e + e = e (ja1j + ja2j + 1) = e0 = ja2j+ja1j+1
(ja1j + ja2j + 1) = e0 which proves the goal. 3
We describe here how the special techniques mentioned in the introduction are used in the course of the proof presented above, namely at the key steps indicated with [K1], . . . , [K5]. 3.1
Here the prover must produce the witness a1 a2 needed for the existential
variable a in the current goal (
In the proof above we used another, much simpler technique: reasoning about terms behaviour in zero. It is clear that the formula (A) expresses the behaviour of the polynomials in any (small) vicinity of zero. Since polynomials are continuous, this will also be their behaviour in zero. One can in fact prove that formula (A) is equivalent to the formula: 8a1;a2 9a0 8x1;x2 (jx1 a1j = 0 ^ jx2 a2j = 0) ) jx1 x2 a0j = 0 In our special case it is immediately clear that a0 equals a1 a2, but we implemented a more general method: the two LHS equations are solved for x1; x2, then the values are replaced in the RHS equation, which is then solved for a0. 3.2
Here the prover must produce an appropriate term for the instantiation of the
assumptions (
Again it is possible to use QE by CAD, by treating the formula (A) after replacing a0 with its value and removal of the quanti ers for a0; a1; a2 { see [1]. This works in the case of sum, but again it does not work satisfactorily in the case of product.
In order to nd this witness (we assume that it is the same for e1 and e2), we use algebraic manipulation (solving, substitution, and computation), as well as rewriting of terms under the absolute value function. This is probably the most interesting of the new techniques presented here, and is detailed below at [K5]. 3.3
The proof needs a witness for the existential variable M in the goal (
The assumptions (12) and (13) need to be instantiated with appropriate terms for the universally quanti ed variable n. Here we use the special heuristics: identi cation of equal terms under unknown functions.
Since f1 and f2 are universally quanti ed in the original formula, and later become arbitrary constants, we do not know anything about their behaviour. In the goal (16), f1 and f2 have argument n0. Therefore it will be possible to use the assumptions (12) and (13) for proving (16) only if f1 and f2 are applied to the same argument. (This corresponds in fact to resolution in rst order logic.) In the case of this proof the solution is to set n to n0, but even if the expressions are more complicated one can use equation solving, substitution, and computation in order to nd more complicated terms. Moreover, after this instantiation we substitute f1[n0] and f2[n0] with new arbitrary constants (e. g. x1, x2, respectively): this makes our expressions polynomial and helps creating the formula (A). 3.5
The most challenging part is the automatic generation of the instantiation term needed at step [K2], which is performed by a heuristic combination of solving, substitution, and simplifying, as well as rewriting of expressions under the absolute value function.
Note that the goal (16) has under the absolute value function the expression (call it E0) corresponding to x1 x2 a1 a2. Let us also name the absolute value arguments of the assumptions (18) and (19) as E1 and E2, respectively.
First we use the following heuristic principle: transform the goal expression E0 such that it uses as much as possible E1 and E2, because about those we know that they are small. In order to do this we take new variables y1; y2, we solve the equations y1 = E1 and y2 = E2 for x1; x2, we substitute the solutions in E0 and the result simpli es to: a1 y2 +a2 y1 +y1 y2. This is the internal representation of the absolute value argument in the goal (20). Note that the transformation from (16) to (20) is relatively challenging even for a human prover.
The formula (21) is realized by rewriting of the absolute value expressions. Namely, we apply certain rewrite rules to expressions of the form jEj and their combination, as well as to the metavariable e. Every rewrite rule transforms a (sub)term into one which is not smaller, so we are sure to obtain a greater or equal term. The nal purpose of these transformations is to obtain a strictly positive ground term t multiplied by the target metavariable (here e). Since we need a value for e which full ls t e e0, we can set e to e0=t. The rewrite rules come from the elementary properties of the absolute value function: (e. g. ju + vj juj + jvj)) and from the principle of bounding the -bounds: Since we are interested in the behaviour of the expressions in the immediated vicinity of zero, the bounds (e; e0; e1; e2) can be bound from above by any positive value. In the case of product (presented here), we also use the rule: e e e, that is we bound e to 1. This is why the nal expression of e is the minimum between 1 and the term t found as above.
This method works of course also for the case of sum of sequences.
In order to make it work for more complex expressions, namely rational functions, we use a second set of rules which decrease the term: in order to obtain a bound for U=V , increase U and decrease V . Using this we obtain automatically appropriate bounds for the case of inverse of a sequence and for the case of fraction of two sequences.
Full detail of the techniques and of the examples are presented in [5]. 3.6
At certain places in the proof, the conditions upon certain quanti ed variables have to be proven. The prover does not display a proof of these simple statements, but just declares them to be consequences of \elementary properties of R". (Such elementary properties are also invoked when developing formulae (20) and (21).) By \elementary properties" in this context we understand the properties of various constants (like 0, 1), functions (like Min, Max, absolute value, +; ; ; =), and predicates (like =; <; ) over reals and naturals, which are normally studied before the notions of limit, continuity, etc. and which are typically considered prerequisites for working in elementary analysis.
In the background, however, the prover uses Mathematica functions in order to check that these statements are correct. This happens for the subgoal (9) and will be treated after the instatiation term is found, by using QE on the formula 8e0 (e0 > 0 ) e > 0) (where e has the found value Min[: : :]), which returns true in Mathematica. The same procedure is used for the subgoal (17). 4
The full automation of proofs in elementary analysis constitutes a very intersting application for the combination of logic and algebraic techniques, which is essentially equivalent to SMT solving (combining satis ability checking and symbolic computation). Our experiments show that complete and e cient automation is possible by using certain heuristics in combination with complex algebraic algorithms.
Further work includes a systematic treatment of various formulae which appear in textbooks, and extension of the heuristics to more general types of formulae. In this way we hope to address the class of problems which are usually subject to SMT solving.