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 rst derivative. In its present (still quanti er-free) version, our decidable language embodies addition of functions; the issue we address is the one of satis ability. As regards real numbers, individual variables and constructs designating the basic arithmetic operations are available, along with comparison relators. As regards functions, we have another sort of variables, out of which compound terms are formed by means of constructs designating addition and|outermostly|di erentiation. An array of predicates designate various 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 signi cant e ort 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 di erentiation) among the constructs of our fragment of mathematical analysis.
This paper addresses the decision problem for a fragment of real analysis which,
besides the four operators `+', ` ', ` ', `=' of elementary real algebra, also
provides predicates expressing strict and non-strict monotonicity, concavity, and
convexity of C1 functions of one real variable over bounded or unbounded
intervals, 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
differentiation operator whose usage must be reasonably restrained.5 The language
under study, named RDF , is devoid of quanti ers; we reduce the satis ability
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. [
Our decision method consists in preprocessing the given formula into an equi-satis able quanti er-free formula of the elementary algebra of real numbers, whose satis ability 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 satis ability-preserving, we must gure out a exible-enough family of interpolating C1 functions that can accommodate a model for the source formula whenever the target formula turns out to be satis able.
This paper is a sequel of [
Our present language RDF di ers from the language RDF + studied in
[
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 di erentiation operator D[ ] can only appear as the lead operator in a function term g (which will then coincide with D[ f ]). The rationale is that D[ f ] might not designate a C1 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 . 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 a ord to specify it in detail, we exemplify its use by manually working out an emulation of how it would process a speci c, 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 Di erentiable Functions, is an unquanti ed rst-order theory dealing with reals and with real functions of class C1 of one real variable, namely functions with continuous rst derivative. The function symbols of RDF designate the basic operations of real arithmetic, and pointwise addition and di erentiation of functions. Its predicate symbols designate: comparisons between reals, pointwise comparisons of functions; strict and non-strict monotonicity, convexity, and concavity; comparisons between rst derivatives and real terms. This section introduces the language underlying RDF , explains its intended meaning, and brie y illustrates its use.
The language RDF has two in nite 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 C1(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 +1 and 1, occurring only as ends of interval speci cations (see below).
We next specify the syntax of terms, atoms, and formulas for RDF : De nition 1. Function terms, numerical terms, and interval specs are so de ned: 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. 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 1, and e2 for either a numerical term or +1; c.2) we dub the \extended" numerical terms e1; e2 of such an A the ends of
A . a De nition 2. An atom of RDF is an expression of one of the forms s = t ; (f = g)A ;
Up(f)A ;
Down(f)A ; Convex(f)A ; Concave(f)A ;
s > t ; (f > g)A ;
Strict Up(f)A ;
Strict Down(f)A ; Strict Convex(f)A ; Strict Concave(f)A ; (D[f] ./ t)A ; where ./ 2 f=; <; >; 6; > g and A stands for an interval spec. A formula of RDF is any truth-functional combination of RDF atoms. a For de niteness, 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 de nition, with which any truth-value assignment for the formulas of RDF must comply.
De nition 3. An assignment for RDF is a mapping M whose domain consists 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 de ned di erentiable 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 2 f+; ; g, 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 speci cally, for numerical variables and function variables. 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 speci cation 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 i M s = M t (resp. M s > M t) holds; b) (f = g)A is true i (M f)(x) = (M g)(x) holds for all x in M A; c) (f > g)A is true i (M f)(x) > (M g)(x) holds for all x in M A; d) (D[f] ./ t)A, with ./2 f=; <; >; 6; >g, is true i D[(M f)](x) ./ M t holds for all x in M A; e) Up(f)A (respectively Strict Up(f)A) is true i (M f) is a monotone nondecreasing (resp. strictly increasing) function in M A; f) Convex(f)A (respectively Strict Convex(f)A) is true i (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 de ned 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
for every ' in .
of formulas when M ' is true
De nition 4 (Derived symbols). In light of the above semantics, we tacitly
enrich our language, much as in [
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 de nitions.
Among others, any function of the form x 7! q x+q0, with q and q0 xed rational
numbers, can be characterized by means of a formula as in [
| n t{izmes } f ] 1;+1[ $Def zg + }| + g{ = zf + }| + f{ ; + g + f +
+ f = 0: | m {tizmes } 9 It goes without saying what is meant when M is unde ned at either end of A (actually, M ( 1) and M (+1) are unde ned). a a 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(a) )[a;b] $ Linear(f )[a;b], where an equivalence b a holds when the derivative is equal to the di erence 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 2 ]a; b[ , then f is monotone increasing in [a; b].
I b > a ^ (b a) t = f (b) f (a)
! 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(a) holds. b a This is a weak version of Lagrange's mean value theorem. : (D[f ] 6= t)]a;b[ 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 is 2 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 rst three
could also be handled by the simpler decision algorithm tailored for RDF + (cf.
[
As announced in the Introduction, a satis able RM CF + formula may cease
to be satis able in RDF . Such a formula is (see [
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 C1 class. 2
Establishing that an RDF formula is valid amounts to establishing that its negation : is not satis able; moreover, satisfying : amounts to satisfying one of the disjuncts of its disjunctive normal form, hence the key issue concerning 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 satis able? Via routinary attening techniques and in view of some basic properties of C1, we can restate each instance of this problem as the one of determining the satis ability of an arbitrary conjunction '0 of atoms of the forms z = x + y ; z = x y ; x > y ; (h = f + g)A ; (f = g)A ; (f > g)A ; z = f (x) ;
Strict Down(f )A ; (D[f ] ./ z)A ; z = D[f ](x) ;
Concave(f )A ;
Strict Convex(f )A ;
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, 1, or +1; 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 satis ability by means of Tarski's celebrated decision algorithm [
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] o ers 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; y0 subject to constraints v 6 x < x0 6 w ^ y = f (x) ^ y0 = f (x0) ^ y > y0. 3. With certain salient variables vj in the domains of the functions designated by the function variables in '0, associate new variables yjf , tjf (one for each function variable f ) subject to the constraints yjf = f (vj ), tjf = D[f ](vj ). 4. Get rid of all literals involving function variables, whose graphs are already outlined by the variables yjf , tjf introduced above. This elimination phase calls for the introduction of new variables subject to suitable algebraic constraints.
Our decision algorithm for RDF cannot be speci ed 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] ^ is true under every value assignment; equivalently, we can check whether its negation : is unsatis able. 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 function variable of ' and v for one of its so-called `domain' variables. More precisely, 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] ^ v1 6 v2 6 v3 ^ h(v1) = yh
1 ^ D[h](v1) = t1h ^
f (v1) = y1f ^ D[f ](v1) = tf1g ^
g(v1) = y D[g](v1) = t1g1 ^^
D[g] = s [v1;v3] ^ h = f + g [v1;v3] ^ D[h](v2) = y ^ p = r + s ^ y 6= p ^ h(v2) = y2h ^ h(v3) = y3h ^ D[h](v2) = t2h ^ D[h](v3) = t3h ^ y = t2h ^
f (v2) = y2f ^ f (v3) = y3f ^
DDg[[fg(v]]((2vv)22=))==y2gttg2f2 ^^^ DDg[[gf(]v]((3vv)33)=)==y3gttg3f3: ^^ 4. Elimination of function variables: This nal phase removes all literals still containing function variables. We get rid of them by suitable replacements involving algebraic conditions, such as the di erence quotient for literals regarding derivatives. For example, the literal D[f ] = r [v1;v3] becomes the conjunction tf1 = r ^ tf2 = r ^ tf3 = r ^ yv2f2 vy11f = r ^ yv3f3 vy22f = r; where the tif 's represent salient values of the derivative and yvifi++11 yvifi = r the corresponding di erence quotients. To make the manner we eliminate the \function literals" clearer we mark with the same color the two literals f + g [v1;v3] and their transformations.
At the end we obtain an equisatis able Tarskian formula we can then test for satis ability by Tarski's algorithm.
From the previous formula '3 we get the following nal formula '4: y 6= p tf3 = r tg3 = s ^ ^ ^
y =f t2h yv2f2 vy11 = r y2g yg v2 v11 = s ^ ^ yv3f3 vy22f = r ^
y3g yg ^ v3 v22 = s ^ y2h = y2f + y2 ^ g y3h = y3f + y3g ^ 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 satis ability preserving. Regarding the rst 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 equisatis ability 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 una ordably 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 variables.
Soundness: If a model exists for '3, it can be extended to a model that also
veri es the numerical formulas added in '4, since these formulas re ect
properties of the functions in '3 at speci c points of real intervals.
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 a ected 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 parabfolic perturbations to satisfy
constraints on derivatives, such as D[f ](vi) = ti . 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
[
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 quanti er-free formula of the elementary algebra of real numbers:
v1 = 0 ^ v2 = 1 ^ y1f = 0 ^ y2f = 3 ^ tf1 = 1 ^ tf2 = 0 : Driven by this satis able formula, we want to construct an appropriate C1 function 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 rst 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 de ned on the interval 0; 12 , of the form:
1 n G[k; 1; 2](x) := (1 4k)2 (1
4k)[ 2 2k ( 1 + 2)]x + 2k( 1 2)(1 2k) 2k p2p2k2 + (1 4k) x o ; 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 re ections, translations and dilations, we can de ne all required perturbations.
3*x f(x) 3 2 2.5 1.5
1
0.5
0
0
0.2
0.4
0.6
0.8
1
In the example we are considering, after entering the right values for the
derivative, we obtain the function
where 3 x is the linear part and the rest speci es the parabolic perturbation.
The graph of this function (whose rst half falls directly under G[k; 1; 2](x),
while the second half results from that scheme through appropriate
manipulations) can be seen below.
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 +
[
Since the decidability of RDF is obtained via an explicit algorithm, some
complexity issues are worth being discussed here. Tarski's decision method
enters into ours, hence our algorithm inherits its complexity as a lower bound. The
rst complexity amelioration w.r.t. Tarski's historical result is due to Collins
[
Finally, while Tarski himself showed that decidability of his full elementary
algebra of real numbers [
This article has presented a decision algorithm for a syntactically delimited fragment, RDF , of real analysis. RDF extends the unquanti ed 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 equisatis able 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 equisatis ability of formulas ' and , and we have sketched the salient points of this correctness proof. The proof relies upon the construction of a set of C1 functions rich enough to enable the modeling of any satis able 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
operator 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
multivariable 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 [