We enrich a pre-existing decision algorithm, which in its turn augmented a fragment of Tarski's elementary algebra with one-argument functions enjoying signi cant properties such as continuity and di erentiability. We also pave the way to further enrichments, embodying symbols to designate certain operations on functions such as pointwise addition.
Around 1930, Alfred Tarski put forward an axiomatic system of elementary
geometry based on rst-order predicate calculus and proved, through a quanti
erelimination method, the completeness of his axiomatic theory. Completeness
entailed the algorithmic solvability of the truth problem as referred to sentences in
the elementary algebra of real numbers [
Let us brie y explain the basic idea through which one gets the decidability of RMFC, RM F C , RDF, and RDF . As a preliminary, notice that if Dx1 : : : Dxn is an existential sentence of EAR, the elementary algebra of real numbers, and hence is a quanti er-free formula all of whose free variables are among x1; : : : xn, then is true i there exist real numbers a1; : : : ; an which satisfy , to wit, i is satis able; and, since by Tarski's result we have a decision algorithm for existential sentences of EAR, we also have a satis ability algorithm for quanti er-free formulas of EAR. All four theories mentioned above extend the existential fragment of EAR with a new sort of variables, for functions, and with new predicate symbols, for special relations regarding functions; in order to establish their decidability, we translate their formulas into logically equivalent formulas of the existential theory of real numbers and thus can rely upon Tarski's original decision result. 2
The RDF
The augmented version RDF of the theory RDF of reals with di erentiable functions, is an unquanti ed rst-order theory involving various predicates on real functions of class C1 of one real variable, namely functions with continuous rst derivative. Predicates of RDF concern comparison of functions, strict and non-strict monotonicity, strict and non-strict convexity (and concavity), and comparison of rst derivatives with real constants. In this section we introduce the language of RDF , explain its intended meaning, and illustrate its use through quick examples.
The RDF language involves variables of two di erent sorts: numerical variables, denoted by x; y; : : : , range over numbers; functional variables, denoted by f; g; : : : , range over functions. Six constants are also available: { the symbols 0 and 1, designating the numbers 0 and 1; { the symbols 8 and 8, occurring only as endpoints of interval domains (whose de nition will be given later);
We next specify the syntax of term, atom, and formula for RDF : De nition 21 Numerical terms are recursively de ned as follows: 1. numerical variables and the constants 0; 1 are numerical terms; 2. if t1 and t2 are numerical terms, then t1 t2 ; t1
t2 ; and t1 t2 also are numerical terms; 3. if t is a numerical term and f is a functional variable, then
f ptq and Drf sptq also are numerical terms; 4. numerical terms are all and only the expressions built up according to the above criteria 1., 2., and 3.
In the ongoing, we will refer by the locution \numerical variable" to either a numerical variable proper or to one of the constants 0 and 1. Moreover, we will refer by the locution \extended numerical variable" to either a numerical variable or one of the symbols 8, 8; and by the locution \extended numerical term" to either a numerical term or one of the symbols 8, 8.
is an expression of one of the forms t1 t2 ; t1 ¡ t2 ; pf gqA ; pf ¡ gqB ;
Concavepf qA ; Strict Concavepf qA ; pDrf s ' tqA ; where: A designates an interval, either bounded or unbounded, open, half-open or closed; B designates a bounded interval, open, half-open, or closed; t1; t2; t are numerical terms, and ' P t ; ; ¡; ¤; ¥ u. Speci cally, A can be of any of the forms re1; e2s, re1; e2r, se1; e2s, se1; e2r, where e1 is either a numerical term or 8, and e2 is either a numerical term or 8; as for B, it can be of any of the forms rs1; s2s, rs1; s2r, ss1; s2s, ss1; s2r, where s1 and s2 are numerical terms. We dub the extended numerical terms e1; e2 ends of A; likewise, we dub the numerical terms s1; s2 ends of B. (When we will come to the semantics|we will call the quantities designated by the ends of an interval speci cation the endpoints of the designated interval).
atoms of RDF . is any truth-functional combination of For de niteness, we will build up the RDF formulas from RDF means of the usual propositional connectives ; ^; _; Ñ; Ø. atoms by Observation 24 (Derived relators) For convenience, we enrich our language with derived symbols by means of the following shortening de nitions: t1 t2 ØDef pt1 t2q ; t1 t2 ØDef t2 ¡ t1 ; t1 ¤ t2 ØDef pt1 t2q _ pt1 t2q ; t1 ¥ t2 ØDef pt1 ¡ t2q _ pt1 t2q ; t1 t2{t3 ØDef pt2 t1 t3q ^ pt3 0q ; t1 ¡ t2{t3 ØDef pt2 t1 t3q ^ pt3 ¡ 0q _ pt2 ¡ t1 t3q ^ pt3 0q ; t1 t2{t3 ØDef pt2 ¡ t1 t3q ^ pt3 ¡ 0q _ pt2 t1 t3q ^ pt3 0q : When A is as in Def. 22, we also introduce the abbreviation:4 pDrf s
tqA ØDef pDrf s tqA _ pDrf s ¡ tqA : Remark 21 Notice that although we have chosen to regard them as primitive constructs, the relators Up ad Down are expressible in terms of di erentiation, via the equivalences:
Uppf qA Ø pDrf s ¥ 0qA _ pe1 Downpf qA Ø pDrf s ¤ 0qA _ pe1 e2q ; e2q ; where e1; e2 are the ends of A .
Constructs which could easily be brought into play as derived relators designate the notions of upward monotonicity in a point and of in ection point : uppf; cq
ØDef pDrf s ¥ 0qrc;cs ; strict uppf; cqrx;ys ØDef x c ^ c y ^ Strict uppf qrx;ys ; expf; cqrx;ys ØDef p x c ^ c y q ^
:
The semantics of RDF (in light of which the above abbreviations should become clear) 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 25 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 additive zero and multiplicative unit; 1. For each numerical variable x, M x is a real number. 2. For each functional variable f , pM f q is an everywhere de ned di erentiable real function of one real variable, endowed with continuous derivative. 3. For each numerical term of the form t1 b t2 with b P t ; ; u, M pt1 b t2q is the real number M t1 b M t2. 4. For each numerical term of the form f ptq; M pf ptqq is the real number pM f qpM tq; for each numerical term Drf sptq; M pDrf sptqq is the real number DrpM f qspM tq. 5. 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.5 For example, when A st1; t2s, then M A sM t1; M t2s. 4 The rationale of the abbreviation pDrf s tqA will become clearer in light of the semantics: in fact, it relies on the continuity of the derivative of f . 5 It goes without saying what is meant when M is unde ned at either end of A (actually, M p 8q and M p 8q are unde ned). 6. Truth values are assigned to formulas of RDF according to the following rules (where t; t1; t2 stand for numerical terms, and f; g for functional variables): a) t1 t2 (resp. t1 ¡ t2) is true i M t1 M t2, (resp. M t1 ¡ M t2); b) pf gqA is true i pM f qpxq pM gqpxq holds for all x in M A; c) pf ¡ gqB is true i pM f qpxq ¡ pM gqpxq holds for all x in M B; d) pDrf s ' tqA, with 'P t ; ; ¡; ¤; ¥u, is true i DrpM f qspxq ' M t holds for all x in M A; e) U ppf qA (resp. Strict U ppf qA) is true i (M f ) is a monotone nondecreasing (resp. strictly increasing) function in M A; f ) Convexpf qA (resp. Strict Convex) is true i (M f ) is a convex (resp.
strictly convex) function in M A; g) the truth values of Downpf qA and Concavepf qA (resp., of Strict Downpf qA and Strict Concavepf qA), are de ned in close analogy with points 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 Remark 22 Notice that when an interval turns out to have a left endpoint greater than or equal to its right endpoint, then it is either empty or a singleton. Accordingly, most atoms involving that interval turn out to be vacuously true: this is the case, e.g., with all atoms of the forms Uppf qrt;ts, Uppf qst;tr,
mulae uppf; tq and strict uppf; tq as introduced in Remark 21 are at times false and at times true).
However, an atom of any of the forms pf gqrt1;t2s ; pf ¡ gqrt1;t2s ; pDrf s tqrt1;t2s ; pDrf s ' tqrt1;t2s ; with t1
t2, can be false.
Example 21 Notice that any constant function x ÞÑ q, where q is a rational constant, can be easily characterized by means of an RDF formula. E.g., when q is a positive integer, such a function can be described by the derived relator: f q : pDrf s 0qs 8; 8r ^ f p0q 1 1 : looooomooooon q times
In analogous terms one can express the fact f is a rst-degree polynomial with xed rational coe cients. E.g. the function x ÞÑ 2x 13 can be de ned as: f Example 22 Let f be a real function de ned in the closed and bounded interval ra; bs, di erentiable with a continuous derivative f 1. If f 1pxq ¡ 0 for all x P sa; br then f is monotone increasing in ra; bs.
This theorem can be translated into the following formula of RDF :
Notice here that the truth of the claim as stated in words amounts to the validity of the RF D formula into which we have translated it, i.e., it amounts to the fact that the RF D formula evaluates to true in any assignment M . Checking automatically that this is indeed the case will be possible by means of the decision algorithm that we are about to describe, as will be illustrated in Sec. 5.
Example 23 Let f be a real function de ned in a closed bounded interval ra; bs, di erentiable with a continuous derivative f 1. Then there is c P sa; br such that f 1pcq fpbbq fapaq .
Here is how we can state this weak version of the mean value theorem in RDF : a b Ñ
Dpf q f pbq b f paq a sa;br : As with the preceding example, the validity of this formula can be established automatically, by means of the decision algorithm to be presented next. 3
When one deals with an unquanti ed language such as RDF , which is closed with respect to propositional connectives, being able to determine algorithmically whether or not a formula is valid amounts to establishing whether the negation thereof is satis able or unsatis able. We prefer to address the satis ability problem for RDF in what follows, and our algorithm will produce a yes/no answer, where `yes' means that ' admits a model. Hence, indirectly, if we were to test a formula for validity, a negative response would mean that a counterexample exists.
The idea is to transform, through a nite number of steps, the given RDF formula ' to be tested for satis ability into a nite collection of formulas i, still devoid of quanti ers, each belonging to the elementary algebra of real numbers; this will be done so that ' is satis able if and only if one of the resulting i is satis able. Each resulting i can be tested via Tarski's decision algorithm.
First we reduce our formula ' to a particular format, called ordered form; second we explain the algorithm.
Let T be an unquanti ed, possibly multi-sorted, rst-order theory, endowed with: equality , a denumerable in nity of individual variables x1; x2; : : : , function symbols F1; F2; : : : , and predicate symbols P1; P2; : : : .
De nition 31 A formula ' of T is said to be in normal form if: (1) every term occurring in ' either is an individual variable or has the form F px1; x2; : : : ; xnq, where x1; x2; : : : ; xn are individual variables and F is a function symbol. (2) every atom in ' either has the form x t, where x and t are an individual variable and a term, or has the form P px1; x2; : : : ; xnq, where x1; x2; : : : ; xn are individual variables and P is a predicate symbol.
Via routinary attening techniques, one proves the following: Lemma 1. There is an e ective procedure to transform any formula ' of T into a formula in normal form so that ' and are equisatis able.
A more restrained format than just \normal form" is de ned here: De nition 32 A formula ' of T is said to be in standard normal form if it is a conjunction of literals of the forms: x y ; x
F px1; : : : ; xnq ; x
y ; P px1; : : : ; xnq ;
P px1; : : : ; xnq ; where x; y; x1; : : : ; xn; stand for individual variables, F for a function symbol, and P for a predicate symbol.
Let S be the class of all formulas of T in standard normal form; the following holds: Lemma 2. T is decidable if and only if S is decidable.
Proof : Clearly any algorithm for formulas in T is also an algorithm for formulas in S. For the converse, suppose that an algorithmic satis ability test for S is available, and let ' be any formula of T . By applying the normalization process to ', we get a formula , in normal form such that ' and ' are equisatis able. We can now bring to disjunctive normal form, thus obtaining a formula 1_ _ where all i's are conjunctions, and we may assume that each i is in standard normal form, because any literal of type x F py1; : : : ; ynq within it can be replaced by the conjunction x z ^ z F py1; : : : ; ynq, where z is a brand new variable. Since ' is satis able Ø is satis able Ø i is satis able for some i and since all transformations used to build conjunctions 1; : : : ; n are e ective, our lemma follows. \[
We are now almost ready to de ne an ordered form for RDF formulas. De nition 33 A domain variable in a formula ' of RDF is a numerical variable x which occurs in ' either as the argument of a term of one of the forms f pxq, Drf spxq, with f a functional variable, or as an end of some interval mentioned in ' (as exempli ed by Convexpf qrx; 8s).
De nition 34 An RDF formula is said to be in ordered form if it is in standard normal form and has the form: ' ^ n 1 © where tx1; : : : ; xnu is the set of all distinct domain variables in '.
RDF , nevertheless the following holds: is a proper subset of
Proof : omitted.
is decidable if and only if RDFord is decidable. \[
We describe next the decision algorithm for satis ability of formulas of RDF . In view of Lemma 3, we assume w.l.o.g. that ' is given in ordered form. The algorithm takes a formula ' of RDF and reduces it, via a series ' ; '1 ; '2 ; '3 ; '4 of transformations, to a formula such that: 1. ' and are equisatis able, 2. is an existentially quanti ed Tarski formula, i.e. it contains only real variables, arithmetic operators ; and predicates ; .
As recalled in the introduction, there exists a decision algorithm for Tarski
formulas (cf. [
In the following, wi denotes a numerical variable, while zi denotes an extended numerical variable.
The series of transformations we need goes as follows: 1. ' ; '1: behavior at the endpoints.
(a) Let a; b be real numbers such that a b, and f; g be real continuous functions in the closed interval ra; bs; then f ¡ g holds in the open interval sa; br if and only if one of the followings holds: i. f ¡ g all over ra; bs; ii. f ¡ g all over ra; br, and f pbq gpbq; iii. f ¡ g all over sa; bs, and f paq gpaq; iv. f ¡ g all over sa; br, and f paq gpaq ^ f pbq gpbq. (a1) We can hence rewrite a conjunct of this or of an alike form, namely an atom of one of the forms
pf ¡ gqsw1;w2r ; pf ¡ gqrw1;w2r ; pf ¡ gqsw1;w2s ; as an equivalent disjunction comprising 4 or just 2 alternatives; in particular: pf ¡ gqsw1;w2r ; pf ¡ gqrw1;w2s _ ppf ¡ gqrw1;w2r ^ f pw2q ppf ¡ gqsw1;w2s ^ f pw1q ppf ¡ gqsw1;w2r ^ f pw1q gpw2qq _ gpw1qq _ gpw1q ^ f pw2q pf ¡ gqrw1;w2r ; pf ¡ gqrw1;w2s _ ppf ¡ gqrw1;w2r ^ f pw2q gpw2qq ; gpw2qq : (a2) Each such rewriting disrupts the structure of the overall formula, which we can readily restore by bringing it again to disjunctive normal form 1 _ 2 _ _ n (where n P t2; 4u) by means of the distributive law
pDrf s ¡ tqs 8;w1s ^ pDrf s ¡ tqrw1;w2r ^ w1 w2 ; where w1 is the rst variable in the ordering of domain variables if w2 is preceded by at least one such variable; otherwise, w1 is a brand new domain variable.
We also perform the specular rewriting:
pDrf s ¡ tqsw1; 8r ; pDrf s ¡ tqsw1;w2s ^ pDrf s ¡ tqrw2; 8r ^ w1 w2 : 6 Notice that when, here as well as in steps (b) and (c) below, a new domain variable happens to enter into play, its position w.r.t. the ordering of the domain variables (see Def. 34) is mandatory.
We proceed similarly also in the two cases:
pDrf s tqs 8;w2r; pDrf s tqsw1; 8r :
By these transformations we obtain an equisatis able formula. (c) Let a; b and t be real numbers and f a function, f P C1pra; bsq. Then f 1 ¡ t in sa; br if and only if one of the following holds: i. f 1 ¡ t in ra; bs, ii. f 1 ¡ t in ra; br and f 1pbq t, iii. f 1 ¡ t in sa; bs and f 1paq t, iv. f 1 ¡ t in sa; br, f 1paq t and f 1pbq t.
The action to be made is similar to the one made under (a), i.e.: (c1) we rewrite conjuncts of the forms
pDrf s ¡ tqsw1;w2r ; pDrf s ¡ tqrw1;w2r ; pDrf s ¡ tqsw1;w2s ; as equivalent disjunctions, for example: pDrf s ¡ tqsw1;w2s ; pDrf s ¡ tqrw1;w2s ppDrf s ¡ tqsw1;w2s ^ Drf spw1q tq ; _ (c2) we bring again the overall formula into disjunctive normal form taking the distributive law into account. (c3) If in a formula three literals pDrf s ¡ tqsw1;w2r; Drf spw1q t, and
domain variables, and there are no domain variables between w1 and w2, we add the following ones: w1 w; w w2 and f pwq z.
By applying rules (a), (b), and (c) to a formula in ordered form, we obtain a nite disjunction of i formula; moreover is satis able if and only if at least one of the i is satis able.
To each i we apply the rest of the algorithm. 2. '1 ; '2: negative-clause removal.
From '1 we construct an equisatis able formula '2 with only positive predicates. The general idea applied in this step is to substitute every negative clause involving a functional symbol with an implicit existential assertion. For the sake of simplicity, in the following: { x; x1; x2; x3; y1; y2; y3 will be numerical variables, new with respect the formula we will be considering, { we will use the notation x ¤ y as a shorthand for x ¤ y when x; y are both numerical variables; otherwise (when either x is 8 or y is 8), x ¤ y stands for 0 0. (a) Replace any literal pf gqrz1;z2s occurring in '1 by the formula: pz1 ¤ x ¤ z2q ^ y1 f pxq ^ y2 gpxq ^ py1 y2q: (b) Replace any literal
pf ¡ gqrw1;w2s occurring in '1 by the formula: pw1 ¤ x ¤ w2q ^ y1 Equisatis ability of the formulas '1 and '2 is straightforward to prove. Using Lemma 2 and Lemma 3 we can normalize '2, to obtain an equivalent formula in ordered form with domain variables v1; v2; : : : ; vr. 3. '2 ; '3: explicit evaluation of functional variables.
This step is preparatory to the elimination of the functional clauses, by explicit evaluation of functional variables over domain variables. For each such variable vj and for every functional variable f occurring in '2, introduce two new numerical variables yjf , tjf and add the literals yjf f pvj q and tjf Drf spvj q to '2. Moreover, for each literal x f pvj q already occurring in '2 add the literal x yjf ; and for each literal x Drf spvj q already occurring in '2 insert the literal x tjf into '3.
The formula '3 resulting at the end of these insertions and the original '2 clearly are equisatis able. 4. '3 ; '4: elimination of functional variables.
As a nal step, we get rid of all literals containing functional variables. De ne the index function ind : V Y t 8; 8u Ñ t1; 2; : : : ; ru over the set tv1; v2; : : : ; vru of distinct domain variables of '3 as follows: indpxq : $ 1 if x & l if x % r if x
8; vl for some l P t1; 2; : : : ; ru;
8: For each functional symbol f occurring in '3, let introduce the new numerical variables 0f ; rf and proceed as follows: a) For each literal pf gqrz1;z2s occurring in '3, add all literals yif yig; tif yig whose subscript i satis es indpz1q ¤ i ¤ indpz2q; moreover, if z1 8 introduce the literal 0f 0g; and if z2 8 introduce the literal rf rg : b) For each literal pf ¡ gqrw1;w2s (resp. pf ¡ gqsw1;w2r, pf ¡ gqrw1;w2r, pf ¡ gqsw1;w2s) occurring in '3, add the following literal:
yif ¡ yig for each indpw1q ¤ i ¤ indpw2q (resp. indpw1q i indpw2q, indpw1q ¤ i indpw2q, indpw1q i ¤ indpw2q). Moreover if w1 w2 as domain variables, in the case pf ¡ gqsw1;w2r (resp. pf ¡ gqrw1;w2r, pf ¡ gqsw1;w2s) add the following literals: f g f g ti ¥ ti ; tj ¤ tj presp. tjf ¤ tjg or ti ¥ ti q f g with i indpw1q and j indpw2q. c) For each literal pDrf s ' yqrz1;z2s occurring in '3, where 'P t ; ; ¡; ¤; ¥u, add the following formulas: tif ' y; yjf 1 vj 1 yjf ' y; vj for each indpz1q ¤ i; j ¤ indpz2q; j indpz2q, and if 'P t¤; ¥u add the formulas: yjf 1 vj 1 yjf vj y
f Ñ ptj
f y ^ tj 1 yq; moreover, if z1 8, introduce the literal 0f ' y; and if z2 8, introduce the literal rf ' y: d) For each literal pDrf s ' yqsw1;w2r (resp. pDrf s ' yqsw1;w2s, pDrf s ' yqrw1;w2r) occurring in '3, where 'P t ; ; ¡; ¤; ¥u, add the formulas: tif ' y; yjf 1 vj 1 yjf ' y vj for each indpw1q ¤ j indpw2q and for each indpw1q i indpw2q (resp. indpw1q i ¤ indpw2q and indpw1q ¤ i indpw2q). e) For each literal Strict Uppf qrz1;z2s (resp. Strict Downpf qrz1;z2s) occurring in '3, add the following literals: for each indpz1q ¤ i; j ¤ indpz2q; j indpz2q; moreover, if z1 8, introduce the literal 0f ¡ 0 presp. q and, if z2 8, introduce the formula rf ¡ 0 presp. q: f ) For each literal Convexpf qrz1;z2s (resp. Concavepf qrz1;z2s) occurring in '3, add the following formulas: for each indpz1q ¤ i indpz2q; moreover, if z1 8 introduce the literal 0f ¤ tf1 presp. ¥q; and, if z2 8, introduce the literal rf ¥ trf presp. ¤q: g) For each literal Strict Convexpf qrz1;z2s (resp. Strict Concavepf qrz1;z2s) occurring in '3, add the following formulas:
yvifi tif 1 presp. ¡q; for each indpz1q ¤ i indpz2q; moreover, if z1 8, introduce the literal 0f tf0 presp. ¡q; and, if z2 8, introduce the literal rf ¡ trf presp. q: h) Drop all literals involving any functional variable.
The formula '4 resulting at the end involves only real variables, hence it can be decided by means of Tarski's method. 4
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 functional variables), this should emerge from the comments in the algorithm description section.
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), which consists as usual 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 functional 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 functional variables with suitable interpolation functions. In particular, in the proof we use a family of interpolation functions constructed as the sum of a linear component with a perturbation (that we call \elastic") piecewise-de ned starting from quadratic and exponential expressions. These functions, and their derivatives, consistently express the properties of '3 at points and real intervals. 5
To see the decision algorithm for RDF at work on a paradigmatic instance, we will carry out one by one the transformations leading from ' to '4, where ' results from negation of the formula
produced in Example 22 at the end of Sec. 2.
To automatically prove that this formula is true under any value-assignment to a; b, and f , we use our algorithm and Tarski's decision method to check the unsatis ability of its opposite statement Obviously, in fact, if no assignment makes the latter formula true, then every assignment makes our claim true. We hence apply the decision algorithm to the conjunction ' just seen.
' ; '1: behavior at ends.
According to action (c), we split the atom pDrf s ¡ 0qsa;br into a disjunction: pDrf s ¡ 0qsa;br ; pDrf s ¡ 0qra;bs _ pDrf s ¡ 0qra;br ^ Drf spbq 0 _ pDrf s ¡ 0qsa;bs ^ Drf spaq _ pDrf s ¡ 0qsa;br ^ Drf spaq 0 ^ Drf spbq 0 0 ; then we rearrange the overall formula into disjunctive normal form: rpDrf s ¡ 0qra;bs ^ Strict Uppf qra;bss _ rpDrf s ¡ 0qra;br ^ Drf spbq 0 ^ Strict Uppf qra;bss _ rpDrf s ¡ 0qsa;bs ^ Drf spaq 0 ^ Strict Uppf qra;bss _ rpDrf s ¡ 0qsa;br ^ Drf spaq 0 ^ Drf spbq 0 ^ Strict Uppf qra;bss; (:) nally, to each disjunct '1 of this formula we apply the rest of the algorithm. For the sake of brevity, let us consider only the rst disjunct.
'1 ; '2: negative-clause removal.
pDrf s ¡ 0qra;bs ^ thus getting our '2.
Strict Uppf qra;bs ; pDrf s ¡ 0qra;bs ^ a ¤ x1 x2 ¤ b
^f px1q y1 ^ f px2q y2 ^ y2 ¤ y1; '2 ; '3: explicit evaluation of functional variables.
To describe the evaluation more transparently, let us rename our variables as follows:
a ; v1; x1 ; v2; x2 ; v3; b ; v4; y1 ; y2; y2 ; y3 ; so that our formula '2 becomes: pDrf s ¡ 0qrv1;v4s ^ v1 ¤ v2 v3 ¤ v4 ^ f pv2q y2 ^ f pv3q We can now evaluate the function f over the domain variables V by adding the necessary literals: y3 ^ y3 ¤ y2: tv1; v2; v3; v4u, '3 : pDrf s ¡ 0qrv1;v4s ^ v1 ¤ v2 v3 ¤ v4 ^ f pv2q y2 ^ f pv3q ^f pv1q y1f ^ f pv2q y2f ^ f pv3q y3f ^ f pv4q y4f ^ y2 ^Drf spv1q tf1 ^ Drf spv2q tf2 ^ Drf spv3q tf3 ^ Drf spv4q y3 ^ y3 ¤ y2 y2f ^f y3 y3f t4 : '3 ; '4: elimination of functional variables.
Finally, we can remove all literals containing functional variables, by substituting suitable clauses in their place. We thus get: '4 : v1 ¤ v2 v3 ¤ v4 ^ y3 ¤ y2 ^ y2
f f f f ^ t1 ¡ 0 ^ t2 ¡ 0 ^ t3 ¡ 0 ^ t4 ¡ 0
yf yf y3f yf y4f yf ^ v22 v11 ¡ 0 ^ v3 v22 ¡ 0 ^ v4 v33 ¡ 0; a formula containing only numerical variables which can be submitted to Tarski's decision method. To see that this '4 is false, just focus on its sub-conjunction v2 v3 ^ y2
f y2 ^ y3
f y3f y3 ^ y3 ¤ y2 ^ v3 y2f ¡ 0 ; v2 whose constraints v2 v3 and y3f y3 ¤ y2 y2f yield that yv3f3 vy22f ¤ 0 . By performing a similar analysis of the remaining three disjuncts of (:), one proves the validity of our example.
The decidability of RDF theory treated above is a follow-up of a series of
previous results, regarding the RMFC, RM F C , and RDF theories [
Since the decidability of RDF is obtained via an explicit algorithm, some
complexity issues are worth being discussed here. Since Tarski's decision method
enters into ours, 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 proved the undecidability of EAR extended
with some real functions [
This article has presented a decision algorithm for a fragment, RDF , of real analysis, which extends the elementary algebra EAR of real numbers with variables designating functions of a real variable endowed with a continuous derivative. After introducing the syntax and semantics of RDF , we have shown how to reduce a generic formula ' of RDF to a logically equivalent formula of EAR, thereby showing the decidability of RDF . The proof of correctness of the decision algorithm relies upon a particular class of functions, the r ; 1; 2sde ned functions.
While writing this article, we began to spot out further promising extensions of the decidable theory. The main next extension we are envisaging will allow one to designate pointwise function addition by means of functional terms of the form f g and to constrain the new functions through atoms such as pf g ¡ tqrw1;w2s.
We gratefully acknowledge partial support from project \STORAGE|Universita degli Studi di Catania, Piano della Ricerca 2020/2022, Linea di intervento 2", and from INdAM-GNCS 2019 and 2020 research funds.