We enrich a pre-existing decision algorithm, which in its turn augmented a fragment of Tarski's elementary algebra with one-argument functions enjoying significant properties such as continuity and differentiability. 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 first-order predicate calculus and proved, through a quantifierelimination 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 [14,15]. Subsequent improvements of the decision algorithm aimed, on the one hand, at making its complexity affordable in special subcases; on the other hand, at broadening its applicability beyond algebra, so as to handle entities and constructs relevant to the realm of real analysis. One of the decidable extensions was the RMFC theory (Theory of Reals with Monotone and Convex Functions), first investigated by D. Cantone, A. Ferro, E.G. Omodeo and J.T. Schwartz [3], whose language extends the existential theory of real numbers with various predicates about real functions. Other decidability results were achieved through ideas close to the ones which had led to the decidability of RMFC ; those results regard: RM F C `(Augmented theory of Reals with Monotone and Convex Functions) by D. Cantone, G. Cincotti and G. Gallo [1], RDF (Theory of Reals with Differentiable Functions) by D. Cantone and G. Cincotti [5,2], and finally the RDF `theory (Augmented Theory of Reals with Differentiable Functions) [5], the subject of this paper.
Let us briefly explain the basic idea through which one gets the decidability of RMFC, RM F C `, RDF, and RDF `. As a preliminary, notice that if ψ " Dx 1 . . . Dx n θ is an existential sentence of EAR, the elementary algebra of real numbers, and hence θ is a quantifier-free formula all of whose free variables are among x 1 , . . . x n , then ψ is true iff there exist real numbers a 1 , . . . , a n which satisfy θ, to wit, iff θ is satisfiable; and, since by Tarski's result we have a decision algorithm for existential sentences of EAR, we also have a satisfiability algorithm for quantifier-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.
The augmented version RDF `of the theory RDF of reals with differentiable functions, is an unquantified first-order theory involving various predicates on real functions of class C 1 of one real variable, namely functions with continuous first derivative. Predicates of RDF concern comparison of functions, strict and non-strict monotonicity, strict and non-strict convexity (and concavity), and comparison of first 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 different 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 definition will be given later);
We next specify the syntax of term, atom, and formula for RDF `:
Definition 21 Numerical terms are recursively defined as follows:
1. numerical variables and the constants 0, 1 are numerical terms; 2. if t 1 and t 2 are numerical terms, then t 1 `t2 , t 1 ´t2 , and t 1 ¨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.
Definition 22 An atom of RDF `is an expression of one of the forms
where: A designates an interval, either bounded or unbounded, open, half-open or closed; B designates a bounded interval, open, half-open, or closed; t 1 , t 2 , t are numerical terms, and ' P t", ă, ą, ď, ě u. Specifically, A can be of any of the forms re 1 , e 2 s, re 1 , e 2 r, se 1 , e 2 s, se 1 , e 2 r, where e 1 is either a numerical term or ´8, and e 2 is either a numerical term or `8; as for B, it can be of any of the forms rs 1 , s 2 s, rs 1 , s 2 r, ss 1 , s 2 s, ss 1 , s 2 r, where s 1 and s 2 are numerical terms. We dub the extended numerical terms e 1 , e 2 ends of A; likewise, we dub the numerical terms s 1 , s 2 ends of B. (When we will come to the semantics-we will call the quantities designated by the ends of an interval specification the endpoints of the designated interval).
Definition 23 A formula of RDF `is any truth-functional combination of atoms of RDF `.
For definiteness, we will build up the RDF `formulas from RDF `atoms by means of the usual propositional connectives , ^, _, Ñ, Ø.
Observation 24 (Derived relators) For convenience, we enrich our language with derived symbols by means of the following shortening definitions:
When A is as in Def. 22, we also introduce the abbreviation:
Remark 21 Notice that although we have chosen to regard them as primitive constructs, the relators Up ad Down are expressible in terms of differentiation, via the equivalences:
Uppf q A Ø pDrf s ě 0q A _ pe 1 " e 2 q , Downpf q A Ø pDrf s ď 0q A _ pe 1 " e 2 q , where e 1 , e 2 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 inflection point: uppf, cq Ø Def pDrf s ě 0q rc,cs , strict uppf, cq rx,ys Ø Def x ă c ^c ă y ^Strict uppf q rx,ys , flexpf, cq rx,ys Ø Def p x ă c ^c ă y q Ŝtrict
Convexpf q sx,cr ^Strict Concavepf q sc,yr ˘_ `Strict Concavepf q sx,cr ^Strict Convexpf q sc,yr ˘˙.
The semantics of RDF `(in light of which the above abbreviations should become clear) revolves around the designation rules listed in our next definition, with which any truth-value assignment for the formulas of RDF `must comply.
Definition 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 defined differentiable real function of one real variable, endowed with continuous derivative. 3. For each numerical term of the form t 1 b t 2 with b P t`, ´, ¨u, M pt 1 b t 2 q is the real number M t 1 b M t 2 . 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 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. 5For example, when A "st 1 , t 2 s, then M A "sM t 1 , M t 2 s.
strictly convex) function in M A; g) the truth values of Downpf q A and Concavepf q A (resp., of Strict Downpf q A and Strict Concavepf q A ), are defined 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 Φ of formulas when M ϕ is true for every ϕ in Φ.
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 q rt,ts , Uppf q st,tr , Strict Uppf q rt,ts , Strict Uppf q st,tr , and variants thereof (on the other hand, formulae 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 " gq rt1,t2s , pf ą gq rt1,t2s , pDrf s " tq rt1,t2s , pDrf s ' tq rt1,t2s , with t 1 " t 2 , 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 " 0q s´8,`8r ^f p0q " 1 `¨¨¨`1 looooomooooon q times
.
In analogous terms one can express the fact f is a first-degree polynomial with fixed rational coefficients. E.g. the function x Þ Ñ 2x ´1 3 can be defined as:
We show next how formulas of RDF `can express basic theorems of analysis.
Example 22 Let f be a real function defined in the closed and bounded interval ra, bs, differentiable with a continuous derivative f 1 . If f 1 pxq ą 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 `:
pDrf s ą 0q sa,br Ñ Strict Uppf q ra,bs .
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 defined in a closed bounded interval ra, bs, differentiable with a continuous derivative f 1 . Then there is c P sa, br such that
Here is how we can state this weak version of the mean value theorem in RDF `:
As with the preceding example, the validity of this formula can be established automatically, by means of the decision algorithm to be presented next.
When one deals with an unquantified 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 satisfiable or unsatisfiable. We prefer to address the satisfiability 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 finite number of steps, the given RDF formula ϕ to be tested for satisfiability into a finite collection of formulas ψ i , still devoid of quantifiers, each belonging to the elementary algebra of real numbers; this will be done so that ϕ is satisfiable if and only if one of the resulting ψ i is satisfiable. 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 unquantified, possibly multi-sorted, first-order theory, endowed with: equality ", a denumerable infinity of individual variables x 1 , x 2 , . . . , function symbols F 1 , F 2 , . . . , and predicate symbols P 1 , P 2 , . . . . Definition 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 px 1 , x 2 , . . . , x n q, where x 1 , x 2 , . . . , x n 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 px 1 , x 2 , . . . , x n q, where x 1 , x 2 , . . . , x n are individual variables and P is a predicate symbol.
Lemma 1. There is an effective procedure to transform any formula ϕ of T into a formula ψ in normal form so that ϕ and ψ are equisatisfiable.
A more restrained format than just "normal form" is defined here:
Definition 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 px 1 , . . . , x n q , x ‰ y , P px 1 , . . . , x n q , P px 1 , . . . , x n q , where x, y, x 1 , . . . , x n , 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 satisfiability 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 equisatisfiable. 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 py 1 , . . . , y n q within it can be replaced by the conjunction x " z ^z " F py 1 , . . . , y n q, where z is a brand new variable. Since ϕ is satisfiable Ø ψ is satisfiable Ø ψ i is satisfiable for some i and since all transformations used to build conjunctions ψ 1 , . . . , ψ n are effective, our lemma follows.
[ \ We are now almost ready to define an ordered form for RDF `formulas.
Definition 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 exemplified by Convexpf q rx,`8s ).
Definition 34 An RDF `formula is said to be in ordered form if it is in standard normal form and has the form:
where tx 1 , . . . , x n u is the set of all distinct domain variables in ϕ.
The family RDF òrd of all ordered formulas of RDF `is a proper subset of RDF `, nevertheless the following holds:
Lemma 3. RDF `is decidable if and only if RDF òrd is decidable.
Proof : omitted.
[ \
The algorithm We describe next the decision algorithm for satisfiability 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 equisatisfiable, 2. ψ is an existentially quantified 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. [15] by Tarski, and [6] by Collins). A decision algorithm for RDF results from integrating Tarski's decision algorithm with the reduction ϕ ; ψ we are going to present.
In the following, w i denotes a numerical variable, while z i 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.
(a 1 ) We can hence rewrite a conjunct of this or of an alike form, namely an atom of one of the forms pf ą gq sw1,w2r , pf ą gq rw1,w2r , pf ą gq sw1,w2s , as an equivalent disjunction comprising 4 or just 2 alternatives; in particular: and then working on each δ i separately in the sequel of this algorithm. (a 3 ) Let w 1 , w 2 be numerical variables and f, g be functional variables.
In each δ i where the literals pf ą gq sw1,w2r , f pw 1 q " gpw 1 q, and f pw 2 q " gpw 2 q occur together, when w 1 ă w 2 as ordered domain variables and there are no domain variables between w 1 and w 2 , we add the literals w 1 ă w, w ă w 2 and f pwq " z, where w and z are new numerical variables. 6 Plainly, the resulting formula and the original one are equisatisfiable. (b) We then rewrite each atom of the form pDrf s ą tq s´8,w2r , where f is a functional variable and t, w 2 are numerical variables, as the formula pDrf s ą tq s´8,w1s ^pDrf s ą tq rw1,w2r ^w1 ă w 2 , where w 1 is the first variable in the ordering of domain variables if w 2 is preceded by at least one such variable; otherwise, w 1 is a brand new domain variable. We also perform the specular rewriting: pDrf s ą tq sw 1 ,`8r ; pDrf s ą tq sw 1 ,w 2 s ^pDrf s ą tq rw 2 ,`8r ^w1 ă w2 .
We proceed similarly also in the two cases: pDrf s ă tq s´8,w2r , pDrf s ă tq sw1,`8r .
By these transformations we obtain an equisatisfiable formula. (c) Let a, b and t be real numbers and f a function, f P C 1 pra, 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 1 pbq " t, iii. f 1 ą t in sa, bs and f 1 paq " t, iv. f 1 ą t in sa, br, f 1 paq " t and f 1 pbq " t. The action to be made is similar to the one made under (a), i.e.: (c 1 ) we rewrite conjuncts of the forms pDrf s ą tq sw1,w2r , pDrf s ą tq rw1,w2r , pDrf s ą tq sw1,w2s , as equivalent disjunctions, for example: pDrf s ą tq sw 1 ,w 2 s ; pDrf s ą tq rw 1 ,w 2 s _ ppDrf s ą tq sw 1 ,w 2 s ^Drf spw1q " tq ;
(c 2 ) we bring again the overall formula into disjunctive normal form taking the distributive law pα _ βq ^γ Ø pα ^γq _ pβ ^γq into account. (c 3 ) If in a formula three literals pDrf s ą tq sw1,w2r , Drf spw 1 q " t, and Drtspw 2 q " t occur together, and are such that w 1 ă w 2 as ordered domain variables, and there are no domain variables between w 1 and w 2 , we add the following ones: w 1 ă w, w ă w 2 and f pwq " z.
The same for pDrf s ă tq sw1,w2r . By applying rules (a), (b), and (c) to a formula ψ in ordered form, we obtain a finite disjunction of ψ i formula; moreover ψ is satisfiable if and only if at least one of the ψ i is satisfiable.
To each ψ i we apply the rest of the algorithm. 2. ϕ 1 ; ϕ 2 : negative-clause removal.
From ϕ 1 we construct an equisatisfiable 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, x 1 , x 2 , x 3 , y 1 , y 2 , y 3 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 " gq rz1,z2s occurring in ϕ 1 by the formula: pz 1 ď x ď z 2 q ^y1 " f pxq ^y2 " gpxq ^ py 1 " y 2 q.
(b) Replace any literal pf ą gq rw1,w2s occurring in ϕ 1 by the formula: pw 1 ď x ď w 2 q ^y1 " f pxq ^y2 " gpxq ^py 1 ď y 2 q,
In the same way we can remove literal on open and semi-open intervals. (c) Replace any literal pDrf s " tq rz1,z2s (resp. ă, ď, ą, ě) occurring in ϕ 1 by the formula:
(d) Replace any literal Strict Up pf q rz1,z2s (resp. Strict Down pf q rz1,z2s ) occurring in ϕ 1 by the formula: Γ ^y1 ě y 2 presp. Γ ^y1 ď y 2 q , where Γ :" pz 1 ď x 1 ă x 2 ď z 2 q ^y1 " f px 1 q ^y2 " f px 2 q.
(e) Replace any literal Convexpf q rz1,z2s (resp. Strict Convex pf q rz1,z2s ) occurring in ϕ 1 by the formula:
Γ ^py 2 ´y1 qpx 3 ´x1 q ą px 2 ´x1 qpy 3 ´y1 q presp. Γ ^py 2 ´y1 qpx 3 ´x1 q ě px 2 ´x1 qpy 3 ´y1 qq , where ∆ :" pz 1 ď x 1 ă x 2 ă x 3 ď z 2 q, Γ :" ∆ ^y1 " f px 1 q ^y2 " f px 2 q ^y3 " f px 3 q.
Literals of the forms Concavepf q rz1,z2s , Strict Concave pf q rz1,z2s are handled similarly.
Equisatisfiability 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 v 1 , v 2 , . . . , v r . 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 v j and for every functional variable f occurring in ϕ 2 , introduce two new numerical variables y f j , t f j and add the literals y f j " f pv j q and t f j " Drf spv j q to ϕ 2 . Moreover, for each literal x " f pv j q already occurring in ϕ 2 add the literal x " y f j ; and for each literal x " Drf spv j q already occurring in ϕ 2 insert the literal x " t f j into ϕ 3 . The formula ϕ 3 resulting at the end of these insertions and the original ϕ 2 clearly are equisatisfiable. 4. ϕ 3 ; ϕ 4 : elimination of functional variables.
As a final step, we get rid of all literals containing functional variables.
Define the index function ind : V Y t´8, `8u Ñ t1, 2, . . . , ru over the set tv 1 , v 2 , . . . , v r u of distinct domain variables of ϕ 3 as follows:
x " v l for some l P t1, 2, . . . , ru, r if x " `8.
For each functional symbol f occurring in ϕ 3 , let introduce the new numerical variables γ f 0 , γ f r and proceed as follows: a) For each literal pf " gq rz1,z2s occurring in ϕ 3 , add all literals y f i " y g i , t f i " y g i whose subscript i satisfies indpz 1 q ď i ď indpz 2 q; moreover, if z 1 " ´8 introduce the literal γ f 0 " γ g 0 , and if z 2 " `8 introduce the literal γ f r " γ g r . b) For each literal pf ą gq rw1,w2s (resp. pf ą gq sw1,w2r , pf ą gq rw1,w2r , pf ą gq sw1,w2s ) occurring in ϕ 3 , add the following literal:
for each indpw 1 q ď i ď indpw 2 q (resp. indpw 1 q ă i ă indpw 2 q, indpw 1 q ď i ă indpw 2 q, indpw 1 q ă i ď indpw 2 q). Moreover if w 1 ă w 2 as domain variables, in the case pf ą gq sw1,w2r (resp. pf ą gq rw1,w2r , pf ą gq sw1,w2s ) add the following literals:
with i " indpw 1 q and j " indpw 2 q. c) For each literal pDrf s ' yq rz1,z2s occurring in ϕ 3 , where 'P t", ă, ą, ď, ěu, add the following formulas:
for each indpz 1 q ď i, j ď indpz 2 q, j " indpz 2 q, and if 'P tď, ěu add the formulas:
moreover, if z 1 " ´8, introduce the literal γ f 0 ' y, and if z 2 " `8, introduce the literal γ f r ' y. d) For each literal pDrf s ' yq sw1,w2r (resp. pDrf s ' yq sw1,w2s , pDrf s ' yq rw1,w2r ) occurring in ϕ 3 , where 'P t", ă, ą, ď, ěu, add the formulas:
for each indpw 1 q ď j ă indpw 2 q and for each indpw 1 q ă i ă indpw 2 q (resp. indpw 1 q ă i ď indpw 2 q and indpw 1 q ď i ă indpw 2 q). e) For each literal Strict Uppf q rz1,z2s (resp. Strict Downpf q rz1,z2s ) occurring in ϕ 3 , add the following literals:
for each indpz 1 q ď i, j ď indpz 2 q, j " indpz 2 q; moreover, if z 1 " ´8, introduce the literal γ f 0 ą 0 presp. ăq and, if z 2 " `8, introduce the formula γ f r ą 0 presp. ăq. f ) For each literal Convexpf q rz1,z2s (resp. Concavepf q rz1,z2s ) occurring in ϕ 3 , add the following formulas:
for each indpz 1 q ď i ă indpz 2 q; moreover, if z 1 " ´8 introduce the literal γ f 0 ď t f 1 presp. ěq, and, if z 2 " `8, introduce the literal γ f r ě t f r presp. ďq. g) For each literal Strict Convexpf q rz1,z2s (resp. Strict Concavepf q rz1,z2s ) occurring in ϕ 3 , add the following formulas:
for each indpz 1 q ď i ă indpz 2 q; moreover, if z 1 " ´8, introduce the literal γ f 0 ă t f 0 presp. ąq, and, if z 2 " `8, introduce the literal γ f r ą t f r 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.
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 functional variables), this should emerge from the comments in the algorithm description section.
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), 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 verifies the numerical formulas added in ϕ 4 , since these formulas reflect properties of the functions in ϕ 3 at specific 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 family of interpolation functions constructed as the sum of a linear component with a perturbation (that we call "elastic") piecewise-defined starting from quadratic and exponential expressions. These functions, and their derivatives, consistently express the properties of ϕ 3 at points and real intervals.
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 pDrf s ą 0q sa,br Ñ Strict Uppf q ra,bs , with a, b numerical variables , 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 unsatisfiability of its opposite statement pDrf s ą 0q sa,br ^ Strict Uppf q ra,bs .
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 ą 0q sa,br into a disjunction: pDrf s ą 0q sa,br ; pDrf s ą 0q ra,bs _ " pDrf s ą 0q ra,br ^Drf spbq " 0 ‰ _ " pDrf s ą 0q sa,bs ^Drf spaq " 0 ‰ _ " pDrf s ą 0q sa,br ^Drf spaq " 0 ^Drf spbq " 0 ‰ ; then we rearrange the overall formula into disjunctive normal form:
rpDrf s ą 0q ra,bs ^ Strict Uppf q ra,bs s _ rpDrf s ą 0q ra,br ^Drf spbq " 0 ^ Strict Uppf q ra,bs s _ rpDrf s ą 0q sa,bs ^Drf spaq " 0 ^ Strict Uppf q ra,bs s _ rpDrf s ą 0q sa,br ^Drf spaq " 0 ^Drf spbq " 0 ^ Strict Uppf q ra,bs s;
(:) finally, to each disjunct ϕ 1 of this formula we apply the rest of the algorithm.
For the sake of brevity, let us consider only the first disjunct.
ϕ 1 ; ϕ 2 : negative-clause removal. In order to remove the literal Strict Uppf q ra,bs , we can perform the rewriting pDrf s ą 0q ra,bs ^ Strict Uppf q ra,bs ; pDrf s ą 0q ra,bs ^a ď x 1 ă x 2 ď b ^f px 1 q " y 1 ^f px 2 q " y 2 ^y2 ď y 1 , thus getting our ϕ 2 . ϕ 2 ; ϕ 3 : explicit evaluation of functional variables. To describe the evaluation more transparently, let us rename our variables as follows:
a ; v 1 , x 1 ; v 2 , x 2 ; v 3 , b ; v 4 , y 1 ; y 2 , y 2 ; y 3 , so that our formula ϕ 2 becomes: pDrf s ą 0q rv1,v4s ^v1 ď v 2 ă v 3 ď v 4 ^f pv 2 q " y 2 ^f pv 3 q " y 3 ^y3 ď y 2 .
We can now evaluate the function f over the domain variables V " tv 1 , v 2 , v 3 , v 4 u, by adding the necessary literals:
ϕ 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:
v4´v3 ą 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
whose constraints v 2 ă v 3 and y f 3 " y 3 ď y 2 " y f 2 yield that y f 3 ´yf 2 v3´v2 ď 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 [3,1,5,2].
A general survey on those results can be found in [4], where, other decidability results on real analysis are also treated, in particular the FS theory [9,10].
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 first complexity amelioration w.r.t. Tarski's historical result is due to Collins [6], 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 [11], applicable to sentences in prenex normal form, whose complexity is doubly exponential relative to the number of quantifier alternations. 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 [8]; however, if one fixes beforehand how many variables can be used, then the algorithmic complexity becomes polynomial [12].
Finally, while Tarski himself proved the undecidability of EAR extended with some real functions [15] (for example sin x), in [13] Richardson proved the undecidability of the existential theory of reals extended with the numbers log 2, π and with the functions e x , sin x.
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 , θ 2 sdefined 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 ą tq rw1,w2s .
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.