A Decidable Theory Treating Addition of Differentiable Real Functions? ?? Gabriele Buriola[0000−0002−1612−0985]1 , Domenico Cantone[0000−0002−1306−1166]2 , Gianluca Cincotti[0000−0001−8460−1708]2 , Eugenio G. Omodeo[0000−0003−3917−1942]3 , and Gaetano T. Spartà[0000−0002−8993−5851]4 1 Dept. of Computer Science, University of Verona, Italy gabriele.buriola@univr.it 2 Dept. of Mathematics and Computer Science, University of Catania, Italy domenico.cantone@unict.it 3 Dept. of Mathematics and Earth Sciences, University of Trieste, Italy eomodeo@units.it 4 Pontificia Università Gregoriana, Rome, Italy g.sparta@unigre.it Abstract. This paper enriches a pre-existing decision algorithm, which in its turn augmented a fragment of Tarski’s elementary algebra with one-argument real functions endowed with continuous first derivative. In its present (still quantifier-free) version, our decidable language embodies addition of functions; the issue we address is the one of satisfiability. As regards real numbers, individual variables and constructs designating the basic arithmetic operations are available, along with comparison rela- tors. As regards functions, we have another sort of variables, out of which compound terms are formed by means of constructs designating addition and—outermostly—differentiation. An array of predicates designate var- ious relationships between functions, as well as function properties, that may hold over intervals of the real line; those are: function comparisons, strict and non-strict monotonicity / convexity / concavity, comparisons between the derivative of a function and a real term. With respect to results announced in earlier papers of the same stream, a significant effort went into designing the family of interpolating functions so that it could meet the new constraints stemming from the presence of function addition (along with differentiation) among the constructs of our fragment of mathematical analysis. Key words: Decidable theories, Tarski’s elementary algebra, Functions of a real variable. MS Classification 2010: 03B25, 26A06. ? Copyright c 2021 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). ?? We gratefully acknowledge partial support from project “STORAGE—Università degli Studi di Catania, Piano della Ricerca 2020/2022, Linea di intervento 2”, and from INdAM-GNCS 2019 and 2020 research funds. 2 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà Introduction This paper addresses the decision problem for a fragment of real analysis which, besides the four operators ‘+’, ‘−’, ‘·’, ‘/’ of elementary real algebra, also pro- vides predicates expressing strict and non-strict monotonicity, concavity, and convexity of C 1 functions of one real variable over bounded or unbounded in- tervals, as well as strict and non-strict comparisons ‘>’ and ‘>’ between real numbers and between functions. Further primitive constructs available in the language are: an operator designating pointwise addition of functions, and a dif- ferentiation operator whose usage must be reasonably restrained.5 The language under study, named RDF ∗ , is devoid of quantifiers; we reduce the satisfiability problem regarding its formulas to the provability problem for purely existential sentences in Tarski’s elementary algebra of real numbers, whose decidability is known since long (cf. [17]). We can thus count upon improved versions of Tarski’s original method. Our decision method consists in preprocessing the given formula into an equi-satisfiable quantifier-free formula of the elementary algebra of real numbers, whose satisfiability can then be checked by means of Tarski’s decision method. No direct reference to functions will appear in the target formula, each function variable having been superseded by a collection of stub real variables; hence, in order to prove that the proposed translation is satisfiability-preserving, we must figure out a flexible-enough family of interpolating C 1 functions that can accommodate a model for the source formula whenever the target formula turns out to be satisfiable. This paper is a sequel of [2] and [1]—hence, indirectly, of their antecedents [4,6]. As for semantics, the language RM CF + studied in [2] differs from the one treated here in that RM CF + refers to continuous functions whereas in RDF ∗ functions are also required to be endowed with continuous derivative: in consequence of this, as will be shown, a satisfiable RM CF + formula may cease to be satisfiable in RDF ∗ .6 As for syntax, the sole significant difference between RM CF + and RDF ∗ is that the former did not provide—as we now do—the differentiation operator. A brief account of the decidability result proposed in [2], with examples of usage of its language, can be found in [15, pp.165–177]. Our present language RDF ∗ differs from the language RDF + studied in [1] in that its syntax is richer. We now have a construct for function addition, whose treatment calls for an enhancement of the decision algorithm, to wit, an enhanced reduction to Tarskian algebra. We thus get closer to a language where one can prove the linearity of differentiation; in fact, our next extension will permit multiplication of functions by numbers. The paper is organized as follows. In Sec. 1 we introduce syntax and semantics of the language of interest, and illustrate its expressive power—partly stemming 5 The differentiation operator D[ ] can only appear as the lead operator in a function term g (which will then coincide with D[ f ]). The rationaleis that D[ f ] might not designate a C 1 function when f does; then, e.g., D D[f] + f would be meaningless. 6 On the positive side, since the universe of functions for RM CF + is richer, any formula judged valid by the decision algorithm for RM CF + is also valid in RDF ∗ . A Decidable Theory Treating Addition of Differentiable Real Functions 3 from the ease with which useful derived constructs can be introduced—through a gallery of small examples. In Sec. 2, we describe our decision algorithm: since we cannot afford to specify it in detail, we exemplify its use by manually working out an emulation of how it would process a specific, valid formula. Then Sec. 3 provides clues on the correctness of the proposed decision algorithm. To end, we outline a comparison with related works, and draw conclusions. 1 The RDF ∗ theory The augmented version RDF ∗ of the theory RDF of Reals with Differentiable Functions, is an unquantified first-order theory dealing with reals and with real functions of class C 1 of one real variable, namely functions with continuous first derivative. The function symbols of RDF ∗ designate the basic operations of real arithmetic, and pointwise addition and differentiation of functions. Its predicate symbols designate: comparisons between reals, pointwise comparisons of func- tions; strict and non-strict monotonicity, convexity, and concavity; comparisons between first derivatives and real terms. This section introduces the language underlying RDF ∗ , explains its intended meaning, and briefly illustrates its use. Syntax and semantics The language RDF ∗ has two infinite supplies of individual variables, belonging to the respective sorts: numerical variables x, y, z, . . . and function variables f, g, h, . . . . Numerical and function variables are supposed to range, respectively, over the set R of real numbers and over the class C 1 (R) of continuous functions with continuous derivative [the collection of functions which interests us]. Four constants are also available: – the symbols 0 and 1, designating the numbers 0 and 1;7 – the distinguished symbols +∞ and −∞, occurring only as ends of interval specifications (see below). We next specify the syntax of terms, atoms, and formulas for RDF ∗ : Definition 1. Function terms, numerical terms, and interval specs are so defined: a.1) every function variable f is a function term; a.2) if f and g are function terms, then f + g is a function term. b.1) Numerical variables and the constants 0, 1 are numerical terms; b.2) if s and t are numerical terms, the following also are numerical terms: s + t , s − t , and s · t ; 7 As will turn out, the constants 0, 1 would be eliminable from our language without loss of expressive power, since z = 0∧u = 1 is the sole solution to u = u·u > z ·z = z. 4 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà b.3) if t is a numerical term and f is a function term, then f(t) and D[f](t) are numerical terms.8 c.1) An interval spec A is an expression of any of the forms [e1 , e2 ] , [e1 , e2 [ , ]e1 , e2 ] , and ]e1 , e2 [ , where e1 stands for either a numerical term or −∞, and e2 for either a numerical term or +∞; c.2) we dub the “extended” numerical terms e1 , e2 of such an A the ends of A. a Definition 2. An atom of RDF ∗ is an expression of one of the forms s=t, s>t, (f = g)A , (f > g)A , Up(f)A , Strict Up(f)A , Down(f)A , Strict Down(f)A , Convex(f)A , Strict Convex(f)A , Concave(f)A , Strict Concave(f)A , (D[f] ./ t)A , where ./ ∈ {=, <, >, 6, > } and A stands for an interval spec. A formula of RDF ∗ is any truth-functional combination of RDF ∗ atoms. a For definiteness, we will construct the RDF ∗ formulas from RDF ∗ atoms by means of the usual propositional connectives ¬, ∧, ∨, →, ↔. The semantics of RDF ∗ revolves around the designation rules listed in our next definition, with which any truth-value assignment for the formulas of RDF ∗ must comply. Definition 3. An assignment for RDF ∗ is a mapping M whose domain con- sists of all terms and formulas of RDF ∗ , satisfying the following conditions: 0. M 0 and M 1 are the real numbers 0 and 1. 1. For each numerical variable x, M x is a real number. 2. For each function variable f , (M f ) is an everywhere defined differentiable real function of one real variable, endowed with continuous derivative.  3. For each function term of the form f + g, the image M (f + g) (r) of any real number r is (M f)(r) + (M g)(r). 4. For each numerical term of the form t1 ⊗ t2 with ⊗ ∈ {+, −, ·}, M (t1 ⊗ t2 ) is the real number M t1 ⊗ M t2 . 8 Throughout, s, t and f, g stand, respectively, for numerical terms and function terms while x, y, z and f, g, h stand, more specifically, for numerical variables and function variables. A Decidable Theory Treating Addition of Differentiable Real Functions 5 5. For each numerical term of the form f(t), M (f(t)) is the real number (M f)(M t); for each numerical term D[f](t), M (D[f](t)) is the real number D[(M f)](M t). 6. For each interval specification A, M A is an interval of R of the appropriate kind, whose endpoints are the evaluations via M of the ends of A.9 For example, when A =]t1 , t2 ], then M A =]M t1 , M t2 ]. 7. Truth values are assigned to formulas of RDF ∗ according to the following rules, where s and t stand for numerical terms and f, g for function terms: a) s = t (respectively s > t) is true iff M s = M t (resp. M s > M t) holds; b) (f = g)A is true iff (M f)(x) = (M g)(x) holds for all x in M A; c) (f > g)A is true iff (M f)(x) > (M g)(x) holds for all x in M A; d) (D[f] ./ t)A , with ./∈ {=, <, >, 6, >}, is true iff D[(M f)](x) ./ M t holds for all x in M A; e) Up(f)A (respectively Strict Up(f)A ) is true iff (M f) is a monotone non- decreasing (resp. strictly increasing) function in M A; f) Convex(f)A (respectively Strict Convex(f)A ) is true iff (M f) is a convex (resp. strictly convex) function in M A; g) the truth values of Down(f)A , Concave(f)A , Strict Down(f)A , and Strict Concave(f)A are defined in close analogy with items e) and f); h) the truth value which M assigns to a formula whose lead symbol is any of ¬, ∧, ∨, →, ↔ complies with the usual semantics of the propositional connectives. An assignment M is said to model a set Φ of formulas when M ϕ is true for every ϕ in Φ. a Definition 4 (Derived symbols). In light of the above semantics, we tacitly enrich our language, much as in [1], with derived dyadic and triadic comparators involving numerical terms t1 , t2 , and t3 ; namely t1 . t2 and t1 ./ t2 /t3 , where . ∈ {6=, <, 6, >} and ./ ∈ {=, <, >, 6, >}. Additional relators intermixing function terms and numerical terms, e.g. the construct (D[f] 6= t)A , can also be introduced by means of shortening definitions. Among others, any function of the form x 7→ q ·x+q 0 , with q and q 0 fixed rational numbers, can be characterized by means of a formula as in [1]; in particular, we may define h = 0 ↔Def (h = h+h)]−∞,+∞[ . Thanks to the availability of function addition, one can now also specify the multiplication of a function f by any fixed rational number ± m n : in fact, for n, m positive integers, we can define: n times m times z }| { z }| { g=m  n · f ]−∞,+∞[ ↔Def g + ··· + g = f + ··· + f , m g = − n · f ]−∞,+∞[ ↔Def g + · · · + g + f + · · · + f = 0. a | {z } | {z } n times m times 9 It goes without saying what is meant when M is undefined at either end of A (actually, M (−∞) and M (+∞) are undefined). 6 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà A gallery of examples heading to Cauchy’s mean value theorem In sight of becoming able to express the classical Cauchy’s mean value theorem— which calls, alas, for a syntactical extension of RDF ∗ —, we formulate in RDF ∗ many basic facts of real analysis: I (D[f ] = t)[a,b] → Linear(f )[a,b] If f is a function with constant derivative in the interval [a, b], then it will be linear in the same interval. With a slight abuse of notation we can improve the result as (D[f ] = f (b)−f b−a (a) )[a,b] ↔ Linear(f )[a,b] , where an equivalence holds when the derivative is equal to the difference quotient. I (D[f ] > 0)]a,b[ → Strict Up(f )[a,b] If f is a real function endowed with continuous derivative f 0 , and f 0 (x) > 0 holds for all x ∈ ]a, b[ , then f is monotone increasing in [a, b].   I b > a ∧ (b − a) · t = f (b) − f (a) → ¬ (D[f ] 6= t)]a,b[ If f is a real function endowed with continuous derivative f 0 , then to any interval ]a, b[ with a < b there belongs a c such that f 0 (c) = f (b)−f b−a (a) holds. This is a weak version of Lagrange’s mean value theorem. I [ Up(f )A ∧ Strict Up(g)A ] → Strict Up(f + g)A If f and g are, over the interval A, respectively monotone non-decreasing and monotone increasing, their sum f + g is monotone increasing on A. I [ Up(f )A ∧ f + g = 0 ] → Down(g)A If f is an increasing function all over the interval A, its additive inverse g decreases over A.      I D[f ] = r A ∧ D[g] = s A → D[f + g] = r + s A If the graphs of f and g, restricted to A, are straight lines with slopes r and s, then the graph of f + g restricted to A is a straight line with slope r + s. Moreover, when the interval A reduces to a single point, this formula states the additive property of derivative over all R. I [ Convex(f )A ∧ Convex(g)A ∧ (h + h = f + g)A ] → Convex(h)A If f and g are two convex functions on A, also their average h = f +g 2 is convex on A. I [ (f > k)A ∧ (g > k)A ∧ (h + h = f + g)A ] → (h > k)A If f and g both exceed the function k on A, so does in its turn their average. Every instance of the formula schemes shown before can be validated by means of the decision algorithm that will be presented. Actually, the first three could also be handled by the simpler decision algorithm tailored for RDF + (cf. [1]), since they do not involve sums of functions. A Decidable Theory Treating Addition of Differentiable Real Functions 7 As announced in the Introduction, a satisfiable RM CF + formula may cease to be satisfiable in RDF ∗ . Such a formula is (see [2]): Convex(f )[0,1] ∧ Convex(f )[1,1+1] ∧ f (0) = f (1 + 1) = 0 ∧ f (1) = 1 ∧ Concave(f )[0,1+1] ; as a matter of fact, no real function satisfying its subformula Convex(f )[0,1] ∧ Convex(f )[1,1+1] ∧ f (0) = f (1 + 1) = 0 ∧ f (1) = 1 belongs to the C 1 class. 2 Clues on the decision algorithm Establishing that an RDF ∗ formula ψ is valid amounts to establishing that its negation ¬ψ is not satisfiable; moreover, satisfying ¬ψ amounts to satisfying one of the disjuncts of its disjunctive normal form, hence the key issue concern- ing the decidability of RDF ∗ is: how can we determine whether or not a given conjunction of RDF ∗ literals (that is, RDF ∗ atoms and negations thereof) is satisfiable? Via routinary flattening techniques and in view of some basic proper- ties of C 1 , we can restate each instance of this problem as the one of determining the satisfiability of an arbitrary conjunction ϕ0 of atoms of the forms z =x+y , (h = f + g)A , Strict Up(f )A , Convex(f )A , z =x·y , (f = g)A , Strict Down(f )A , Concave(f )A , x>y, (f > g)A , (D[f ] ./ z)A , Strict Convex(f )A , z = f (x) , z = D[f ](x) , Strict Concave(f )A and of literals which are the complements of atoms of these forms that involve an interval spec. Here A stands for an interval spec whose ends can be numerical variables, −∞, or +∞; as ever, x, y, z stand for numerical variables and f, g, h stand for function variables. Through a process furcating at various points, ϕ0 will undergo a series ϕ0 ; ϕ1 ; ϕ2 ; ϕ3 ; ϕ4 = ϕ b of transformations, ending in a formula ϕ b where function variables do no longer occur, so that ϕ b can be tested for satisfiability by means of Tarski’s celebrated decision algorithm [17,7]. The proper functioning of this method relies on certain assumptions about the detailed structure of ϕ, easy to ensure, which we must fly over. The transformations ϕi−1 ; ϕi (i = 1, 2, 3, 4) serve the following purposes: 1. Subdivide into cases each literal of the form (f > g)A whose A is not of the form [v, w]. E.g., (f > g)]v,w] offers two choices: f (v) > g(v), f (v) = g(v). 2. Substitute every negative literal with an implicit existential assertion. E.g., ¬Strict Up(f )[v,w] will bring into play new variables x, y, x0 , y 0 subject to constraints v 6 x < x0 6 w ∧ y = f (x) ∧ y 0 = f (x0 ) ∧ y > y 0 . 3. With certain salient variables vj in the domains of the functions designated by the function variables in ϕ0 , associate new variables yjf , tfj (one for each function variable f ) subject to the constraints yjf = f (vj ), tfj = D[f ](vj ). 8 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà 4. Get rid of all literals involving function variables, whose graphs are already outlined by the variables yjf , tfj introduced above. This elimination phase calls for the introduction of new variables subject to suitable algebraic con- straints. The decision algorithm at work Our decision algorithm for RDF ∗ cannot be specified in full in these few pages; to convey a feel of how it works, we consider a paradigmatic formula ψ, and carry out one by one the key transformations leading from ψ to a formula directly submittable to Tarski’s algorithm for elementary real algebra. Suppose that we want to establish whether the formula ψ , h   i  D[f ] = r [a,b] ∧ D[g] = s [a,b] → D[f + g] = r + s [a,b] , is true under every value assignment; equivalently, we can check whether its negation ¬ψ is unsatisfiable. After introduction of convenient stub variables h and p, this negation becomes the following formula ϕ:     D[f ] = r [a,b] ∧ D[g] = s [a,b] ∧ h = f + g [a,b] ∧ ¬ D[h] = p [a,b] ∧ p = r + s . Then ϕ undergoes the following transformations: 1. Behavior at the ends: Generally speaking, function-comparison literals of the form (f > g)A must be bestowed special care, possibly leading to a subcase analysis. Since no such literal appears in our ϕ, this phase produces ϕ1 := ϕ . 2. Negative clause removal: This phase removes the negative literal and obtains ϕ2 from ϕ1 by substituting the conjunction a 6 x 6 b ∧ y = D[h](x) ∧ y 6= p for ¬ D[h] = p [a,b] inside it. 3. Explicit evaluation of function variables: This phase introduces a new variable to designate each function-application term `(v), where ` stands for a func- tion variable of ϕ and v for one of its so-called ‘domain’ variables. More pre- cisely, for each function variable f and each domain variable a, we introduce two new numerical variables yaf , tfa and two literals f (a) = yaf , D[f ](a) = tfa evaluating, respectively, the function f and its derivative f 0 in a. To describe evaluation more transparently, let us do the renaming: a ; v1 , x ; v2 , b ; v3 . From the previous formula ϕ2 , we get the following ϕ3 :    D[f ] = r [v1 ,v3 ] ∧ D[g] = s [v1 ,v3 ] ∧ h = f + g [v1 ,v3 ] ∧ v1 6 v2 6 v3 ∧ D[h](v2 ) = y ∧ p=r+s ∧ y 6= p ∧ h(v1 ) = y1h ∧ h(v2 ) = y2h ∧ h(v3 ) = y3h ∧ D[h](v1 ) = th1 ∧ D[h](v2 ) = th2 ∧ D[h](v3 ) = th3 ∧ y = th2 ∧ f (v1 ) = y1f ∧ f (v2 ) = y2f ∧ f (v3 ) = y3f ∧ f f f D[f ](v1 ) = t1 ∧ D[f ](v2 ) = t2 ∧ D[f ](v3 ) = t3 ∧ g(v1 ) = y1g ∧ g(v2 ) = y2g ∧ g(v3 ) = y3g ∧ D[g](v1 ) = t1 ∧ D[g](v2 ) = t2 ∧ D[g](v3 ) = tg3 . g g A Decidable Theory Treating Addition of Differentiable Real Functions 9 4. Elimination of function variables: This final phase removes all literals still containing function variables. We get rid of them by suitable replacements involving algebraic conditions, such as the difference quotient  for literals regarding derivatives. For example, the literal D[f ] = r [v1 ,v3 ] becomes the y f −y f y f −y f conjunction tf1 = r ∧ tf2 = r ∧ tf3 = r ∧ v22 −v11 = r ∧ v33 −v22 = r, where the tfi ’s yf −y f represent salient values of the derivative and vi+1 i i+1 −vi = r the corresponding difference quotients. To make the manner we eliminate the “function  literals” clearer we mark with the same color the two literals D[f ] = r [v1 ,v3 ] , h =  f + g [v1 ,v3 ] and their transformations. At the end we obtain an equisatisfiable Tarskian formula we can then test for satisfiability by Tarski’s algorithm. From the previous formula ϕ3 we get the following final formula ϕ4 : v 1 6 v2 6 v3 ∧ p=r+s ∧ y 6= p ∧ y = th2 ∧ y2f −y1f y f −y f tf1 = r ∧ tf2 = r ∧ tf3 = r ∧ v2 −v1 = r ∧ v33 −v22 = r ∧ y2g −y1g y g −y g tg1 = s ∧ tg2 = s ∧ tg3 = s ∧ v2 −v1 = s ∧ v33 −v22 = s ∧ y1h = y1f + y1g ∧ y2h = y2f + y2g ∧ y3 = y3f + y3g h ∧ th1 = tf1 + tg1 ∧ th2 = tf2 + tg2 ∧ th3 = tf3 + tg3 . In particular, the unsatisfiability of this last formula is given by the conjunction: y = th2 ∧ th2 = tf2 + tg2 ∧ tf2 = r ∧ tg2 = s ∧ p = r + s ∧ y 6= p. 3 Correctness of the algorithm In order to prove the correctness of the algorithm, it is enough to show that each one of the (terminating) transformations ϕ ; ϕ1 , ϕ1 ; ϕ2 , ϕ2 ; ϕ3 , ϕ3 ; ϕ4 is satisfiability preserving. Regarding the first three of them (behavior at the endpoints, negative-clause removal, explicit evaluation of function variables), this emerges as a rather straightforward fact. We must focus on the equisatisfiability of the formulas ϕ3 and ϕ4 , because the transformation ϕ3 ; ϕ4 is less transparent than the previous ones: we are, in fact, comparing a formula whose predicates regard the behavior of functions in real intervals with another one which only involves relations between numerical variables. Let us sketch the idea behind the proof (the full proof is unaffordably long for a conference paper and relies on various propositions of elementary real analysis). As usual, the proof consists of two parts: soundness and completeness. Recall that ϕ4 is obtained from ϕ3 by adding some formulas that involve only numerical variables, and by removing all predicates which refer to function vari- ables. Soundness: If a model exists for ϕ3 , it can be extended to a model that also verifies the numerical formulas added in ϕ4 , since these formulas reflect proper- ties of the functions in ϕ3 at specific points of real intervals. 10 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà Completeness: Conversely, if there exists a model for ϕ4 , it is possible to extend it to ϕ3 by interpreting the function variables with suitable interpolating functions. In the proof, to perform the interpolation we resort to a family of functions, closed under addition. Each function is constructed by combination of pieces, each of which results from a linear component affected by a so-called ‘perturbation’. In its turn, each perturbation stems from a parabola. On the one hand, we use the linear components to satisfy pointwise properties, such as f (vi ) = yif ; on the other hand, we use parabolic perturbations to satisfy con- straints on derivatives, such as D[f ](vi ) = tfi . Closure under addition of the family of interpolating functions ensures proper treatment of literals involving the sum of functions: actually, if (h = f + g)A is one such literal and F, G, H are the functions interpreting the symbols f, g, h, we must require H = F + G. This non trivial condition forced us to shift from the original approach presented in [1] (where the perturbations were based on exponential functions) to the present one, in which the perturbation of each interpolating segment originates from the envelope of two straight lines in the interval 0, 21 . These novel interpolating  functions, and their derivatives, comply with the properties at points and on real intervals dictated by ϕ3 . Sample function resulting from perturbated linear segments To shed light upon the nature of these interpolating functions, here we give a very simple example. Suppose that we must cope, at the end of the decision algorithm, with the following quantifier-free formula of the elementary algebra of real numbers: v1 = 0 ∧ v2 = 1 ∧ y1f = 0 ∧ y2f = 3 ∧ tf1 = 1 ∧ tf2 = 0 . Driven by this satisfiable formula, we want to construct an appropriate C 1 func- tion f . The interpolation constraints which f must comply with are pointwise conditions, two of which regard its derivative: f (0) = 0, f (1) = 3, f 0 (0) = 1, f 0 (1) = 0 . We can meet the first two with a linear segment, namely r(x) = 3 x, but in order to satisfy the conditions on the derivative we need a suitable perturbation of this linear segment. The basic elements out of which  we build our perturbations are envelope functions defined on the interval 0, 21 , of the form:  n 1 G[k, θ1 , θ2 ](x) := (1−4k)2 (1 − 4k)[θ2 −2k (θ1 + θ2 )]x +  √ p o −2k(θ1 − θ2 )(1 − 2k) 2k − 2 2k 2 + (1 − 4k) x , where k is a shrinking parameter involved in the completeness proof and θ1 , θ2 represent the values of the derivative at endpoints. Starting with these basic elements and through reflections, translations and dilations, we can define all required perturbations. A Decidable Theory Treating Addition of Differentiable Real Functions 11 In the example we are considering, after entering the right values for the deriva- tive, we obtain the function ( √ 3x + 49 x + 32 17 in 0, 12    1 − 1 + 16x f (x) := √ 3x + 11 23 1   4 (x − 1) + 32 ( 17 − 16x − 1) in 2 , 1 , where 3 x is the linear part and the rest specifies the parabolic perturbation. The graph of this function (whose first half falls directly under G[k, θ1 , θ2 ](x), while the second half results from that scheme through appropriate manipula- tions) can be seen below. 3 3*x f(x) 2.5 2 1.5 1 0.5 0 0 0.2 0.4 0.6 0.8 1 Fig. 1. Graph of the interpolating function with f (0) = 0, f (1) = 3, f 0 (0) = 1, f 0 (1) = 0. 4 Related works and complexity issues The decidability of the theory RDF ∗ treated above is a follow-up of a series of previous results, regarding the theories RM CF , RM CF + , RDF , and RDF + [4,2,6,3,1]. A general survey on those results, save the last, can be found in [5], where other decidability results on real analysis are also treated, in particular the FS theory [10,11]. Since the decidability of RDF ∗ is obtained via an explicit algorithm, some complexity issues are worth being discussed here. Tarski’s decision method en- ters into ours, hence our algorithm inherits its complexity as a lower bound. The first complexity amelioration w.r.t. Tarski’s historical result is due to Collins 12 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà [7], whose procedure has doubly exponential complexity relative to the number of variables occurring in the sentence (or just exponential, if the endowment of variables is finite and fixed). A refinement of this result was achieved with Grigoriev’s algorithm [12], applicable to sentences in prenex normal form, whose complexity is doubly exponential relative to the number of quantifier alterna- tions. If we merely focus on the existential theory of reals, the known decision algorithms have a complexity at best exponential relative to the number n of variables [9]; however, if one fixes beforehand how many variables can be used, then the algorithmic complexity becomes polynomial [13]. Finally, while Tarski himself showed that decidability of his full elementary algebra of real numbers [17] would be disrupted if the language were enriched with certain real functions, in particular sin x, Richardson proved in [14] the undecidability of the existential theory of reals extended with the numbers log 2 and π, and with the functions ex , sin x. 5 Conclusions and Future Works This article has presented a decision algorithm for a syntactically delimited frag- ment, RDF ∗ , of real analysis. RDF ∗ extends the unquantified part of Tarski’s elementary algebra EAR of real numbers with variables designating functions of a real variable endowed with a continuous derivative. After showing how to add derived relators and how to specify common properties of real functions and theorems about them in RDF ∗ , we have discussed an algorithm that translates a generic formula ϕ of RDF ∗ into an equisatisfiable formula ψ of EAR; rather than specifying the algorithm in gory detail, we have illustrated its functioning through a concrete example. Proving the correctness of the decision algorithm amounts to showing the equisatisfiability of formulas ϕ and ψ, and we have sketched the salient points of this correctness proof. The proof relies upon the construction of a set of C 1 functions rich enough to enable the modeling of any satisfiable RDF ∗ formula: each function results from smoothly connecting linear segments perturbated by means of parabolic deformations. While working on the algorithm we glimpse further extensions. The nearest two amount to a product operator and multi-variable functions. The product oper- ator concerns the assembly of new function terms by multiply function terms and numerical terms. This new construct will enable us to treat literals of the form f = tg A and paves the way to state stronger analytic theorems, such as Cauchy’s mean value theorem. Whereas this “syntactical scalar product” seems easily treatable, combining product of two function terms, such as h = f · g with function sum is likely to disrupt decidability (much as Presburger’s vs. Peano’s arithmetic [9, p.4]), or required at least deep changes in the algorithm. By multi- variable functions we mean the possibility to treat continuous real functions with multiple arguments, such as f : Rn → R. A similar enrichment has already been introduced for the RM CF in [4]. A Decidable Theory Treating Addition of Differentiable Real Functions 13 References 1. Buriola G., Cantone D., Cincotti G., Omodeo E.G., Spartà G.T., A decidable theory of differentiable functions with convexities and concavities on real intervals. In Francesco Calimeri, Simona Perri, and Ester Zumpano, editors, Proceedings of the 35th Italian Conference on Computational Logic - CILC 2020, Rende, Italy, October 13-15, 2020, volume 2710 of CEUR Workshop Proceedings, pages 231–247. CEUR-WS.org, 2020. 2. Cantone D., Cincotti G., Gallo G., Decision algorithms for fragments of real analy- sis. I. Continuous functions with strict convexity and concavity predicates. J. Symb. Comput., 41(7):763-789, 2006. 3. Cantone D., Cincotti G., Decision algorithms for fragments of real analysis. II. A theory of differentiable functions with convexity and concavity predicates. List of CILC 2007 papers, 14 pp., 2007. https://www.programmazionelogica.it/ wp-content/uploads/2014/10/cilc2007.pdf 4. Cantone D., Ferro A., Omodeo E.G., Schwartz J.T., Decision algorithms for some fragments of analysis and related areas. Comm. Pure Appl. Math., 40(3):281-300, 1987. 5. Cantone D., Omodeo E.G., Spartà G.T., Solvable (and unsolvable) cases of the decision problem for fragments of analysis. Rend. Istit. Mat. Univ. Trieste, 44:313- 348, 2012. 6. Cincotti G., Decision algorithms for fragments of real analysis and graph theory, Ph.D. Thesis, Università degli Studi di Catania, Catania, Italy, ix+136 pp., 2000. 7. Collins G., Quantifier elimination for real closed fields by cylindrical algebraic de- composition. In: Second GI Conference on Automata Theory and Formal Lan- guages, LNCS Vol.33, Springer-Verlag, Berlin, 1975. 8. Ferro A., Omodeo E.G., Schwartz J.T., Decision procedures for elementary sublan- guages of set theory. I. Multi-level syllogistic and some extensions, Comm. Pure Appl. Math, 33(5):599–608, 1980. 9. Fisher M. J. and Rabin M. O., Super-exponential complexity of Presburger arith- metic. Complexity and Computation, Vol. VII, SIAM-AMS, Philadelphia (1974), 27–41. 10. Friedman H. and Seress Á., Decidability in elementary analysis. I, Adv. Math. 76 (1989), no. 1, 94–115. 11. Friedman H. and Seress Á., Decidability in elementary analysis. II, Adv. Math. 79 (1990), no. 1, 1–17. 12. Grigoriev D., Complexity of deciding Tarski algebra, J. Symbolic Comput. 5 (1988), 65–108. 13. Renegar J., A faster PSPACE algorithm for deciding the existential theory of the reals, 29th Annual Symposium on Foundations of Computer Science (FOCS 1988, Los Angeles, Ca., USA), IEEE Computer Society Press, Los Alamitos (1988), pp. 291–295. 14. Richardson D., Some undecidable problems involving elementary functions of a real variable, J. Symbolic Logic 33 (1968), 514–520. 15. Schwartz JT, Cantone D, Omodeo EG. Computational logic and set theory: Ap- plying formalized logic to analysis. Springer-Verlag, 2011. ISBN 978-0-85729-807-2. https://doi.org/10.1007/978-0-85729-808-9. Foreword by M. Davis. 16. Tarski A., The completeness of elementary algebra and geometry, Institut Blaise Pascal, Paris, 1967, iv+50 pp. (Late publication of a paper which had been sub- mitted for publication in 1940) 14 G. Buriola, D. Cantone, G. Cincotti, E.G. Omodeo, and G.T. Spartà 17. Tarski A., A decision method for elementary algebra and geometry, prepared for publication by J.C.C McKinsey, U.S Air Force Project RAND, R-109, the RAND Corporation, Santa Monica, 1948, iv+60 pp.; a second, revised edition was pub- lished by the University of California Press, Berkeley and Los Angeles, CA, 1951, iii+63 pp.