=Paper=
{{Paper
|id=Vol-2710/paper15
|storemode=property
|title=A Decidable Theory of Differentiable Functions with Convexities and Concavities on Real Intervals
|pdfUrl=https://ceur-ws.org/Vol-2710/paper15.pdf
|volume=Vol-2710
|authors=Gabriele Buriola,Domenico Cantone,Gianluca Cincotti,Eugenio G. Omodeo,Gaetano T. Spartà
|dblpUrl=https://dblp.org/rec/conf/cilc/BuriolaCCOS20
}}
==A Decidable Theory of Differentiable Functions with Convexities and Concavities on Real Intervals==
https://ceur-ws.org/Vol-2710/paper15.pdf
A Decidable Theory of Differentiable Functions
with Convexities and Concavities on Real
Intervals‹
Gabriele Buriola, Domenico Cantoner0000´0002´1306´1166s1 ,
Gianluca Cincottir0000´0001´8460´1708s1 ,
Eugenio G. Omodeor0000´0003´3917´1942s2 , and Gaetano T. Spartà3
1
Dept. of Mathematics and Computer Science, University of Catania, Italy
domenico.cantone@unict.it
2
Dept. of Mathematics and Earth Sciences, University of Trieste, Italy
eomodeo@units.it
3
Pontificia Università Gregoriana, Rome, Italy
Abstract. 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 differ-
entiability. We also pave the way to further enrichments, embodying
symbols to designate certain operations on functions such as pointwise
addition.
Key words: Decidable theories, Tarski’s elementary algebra, Functions
of a real variable.
MS Classification 2010: 03B25, 26A06.
1 Introduction
Around 1930, Alfred Tarski put forward an axiomatic system of elementary ge-
ometry based on first-order predicate calculus and proved, through a quantifier-
elimination method, the completeness of his axiomatic theory. Completeness en-
tailed 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 Re-
als with Monotone and Convex Functions), first investigated by D. Cantone, A.
Ferro, E.G. Omodeo and J.T. Schwartz [3], whose language extends the existen-
tial 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
‹
Copyright c 2020 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
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. Can-
tone 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 ψ “
Dx1 . . . Dxn θ 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 x1 , . . . xn , then ψ is true iff there exist real numbers a1 , . . . , an 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.
2 The RDF ` Theory
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.
Syntax and semantics
The RDF ` language involves variables of two different sorts: numerical vari-
ables, 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 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.
Definition 22 An atom of RDF ` is an expression of one of the forms
t1 “ t2 , t1 ą t2 ,
pf “ gqA , pf ą gqB ,
Uppf qA , Strict Uppf qA ,
Downpf qA , Strict Downpf qA ,
Convexpf qA , Strict Convexpf qA ,
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. Specifically, A can be of any of the
forms re1 , e2 s, re1 , e2 r, se1 , e2 s, se1 , e2 r, 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 , s2 s, rs1 , s2 r, ss1 , s2 s, ss1 , s2 r, 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 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:
t1 ‰ t2 ØDef pt1 “ t2 q ,
t1 ă t2 ØDef t2 ą t1 ,
t1 ď t2 ØDef pt1 ă t2 q _ pt1 “ t2 q ,
t1 ě t2 ØDef pt1 ą t2 q _ pt1 “ t2 q ,
t1 “ t2 {t3 ØDef pt
` 2 “ t1 ¨ t3 q ^ pt3 ‰ 0q ,˘ ` ˘
t1 ą t2 {t3 ØDef pt2 ă t1 ¨ t3 q ^ pt3 ą 0q _ pt2 ą t1 ¨ t3 q ^ pt3 ă 0q ,
` ˘ ` ˘
t1 ă t2 {t3 ØDef pt2 ą t1 ¨ t3 q ^ pt3 ą 0q _ pt2 ă t1 ¨ t3 q ^ 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 differentiation,
via the equivalences:
Uppf qA Ø pDrf s ě 0qA _ pe1 “ e2 q ,
Downpf qA Ø pDrf s ď 0qA _ pe1 “ e2 q ,
where e1 , e2 are the ends of A .
Constructs which could easily be brought into play as derived relators desig-
nate the notions of upward monotonicity in a point and of inflection point:
uppf, cq ØDef pDrf s ě 0qrc,cs ,
strict uppf, cqrx,ys ØDef x ă c ^ c ă y ^ Strict uppf qrx,ys ,
flexpf, cqrx,ys ØDef p x ă c ^ c ă y q ^
ˆ
` ˘
Strict Convexpf qsx,cr ^ Strict Concavepf qsc,yr _
˙
` ˘
Strict Concavepf qsx,cr ^ Strict Convexpf qsc,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 con-
sists 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 t1 b t2 with b P t`, ´, ¨u, M pt1 b t2 q 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 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.5 For
example, when A “st1 , t2 s, then M A “sM t1 , M t2 s.
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 undefined at either end of A
(actually, M p´8q and M p`8q are undefined).
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 vari-
ables):
a) t1 “ t2 (resp. t1 ą t2 ) is true iff M t1 “ M t2 , (resp. M t1 ą M t2 );
b) pf “ gqA is true iff pM f qpxq “ pM gqpxq holds for all x in M A;
c) pf ą gqB is true iff pM f qpxq ą pM gqpxq holds for all x in M B;
d) pDrf s ’ tqA , with ’P t“, ă, ą, ď, ěu, is true iff DrpM f qspxq ’ M t holds
for all x in M A;
e) U ppf qA (resp. Strict U ppf qA ) is true iff (M f ) is a monotone nonde-
creasing (resp. strictly increasing) function in M A;
f ) Convexpf qA (resp. Strict Convex) is true iff (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 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 single-
ton. 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 ,
Strict Uppf qrt,ts , Strict Uppf qst,tr , and variants thereof (on the other hand, for-
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 ,t2 s , pf ą gqrt1 ,t2 s , pDrf s “ tqrt1 ,t2 s , pDrf s ’ tqrt1 ,t2 s ,
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 “ 1looooomooooon
` ¨¨¨ ` 1 .
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 ´ 31 can be defined as:
f “ 2x ´ 31 :“ pDrf s “ 1 ` 1qs´8,`8r ^ f p0q “ p0 ´ 1q ¨ 1`1`1
1
.
Some examples
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 ą 0qsa,br Ñ Strict Uppf qra,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
f 1 pcq “ f pbq´f
b´a
paq
.
Here is how we can state this weak version of the mean value theorem in RDF ` :
ˆ ˙
f pbq ´ f paq
aăb Ñ Dpf q ‰ .
b´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 The decision algorithm
When one deals with an unquantified language such as RDF ` , which is closed
with respect to propositional connectives, being able to determine algorithmi-
cally whether or not a formula is valid amounts to establishing whether the
negation thereof is satisfiable or unsatisfiable. We prefer to address the satisfi-
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 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.
Normalization
Let T be an unquantified, possibly multi-sorted, first-order theory, endowed with:
equality “, a denumerable infinity of individual variables x1 , x2 , . . . , function
symbols F1 , F2 , . . . , and predicate symbols P1 , P2 , . . . .
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 px1 , x2 , . . . , xn q, 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 in-
dividual variable and a term, or has the form P px1 , x2 , . . . , xn q, where
x1 , x2 , . . . , xn are individual variables and P is a predicate symbol.
Via routinary flattening techniques, one proves the following:
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 px1 , . . . , xn q , x ‰ y ,
P px1 , . . . , xn q , P px1 , . . . , xn q ,
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 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 py1 , . . . , yn q within it can be
replaced by the conjunction x “ z ^ z “ F py1 , . . . , yn 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 qrx,`8s ).
Definition 34 An RDF ` formula is said to be in ordered form if it is in
standard normal form and has the form:
n´1
ľ
ϕ ^ pxi ă xi`1 q,
i“1
where tx1 , . . . , xn u is the set of all distinct domain variables in ϕ.
`
The family RDFord 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 RDFord 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 vari-
ables, arithmetic operators `, ˚ and predicates “, ă.
As recalled in the introduction, there exists a decision algorithm for Tarski for-
mulas (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, wi denotes a numerical variable, while zi denotes an ex-
tended 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 ,w2 r , pf ą gqrw1 ,w2 r , pf ą gqsw1 ,w2 s ,
as an equivalent disjunction comprising 4 or just 2 alternatives; in
particular:
pf ą gqsw1 ,w2 r ; pf ą gqrw1 ,w2 s _
ppf ą gqrw1 ,w2 r ^ f pw2 q “ gpw2 qq _
ppf ą gqsw1 ,w2 s ^ f pw1 q “ gpw1 qq _
ppf ą gqsw1 ,w2 r ^ f pw1 q “ gpw1 q ^ f pw2 q “ gpw2 qq ,
pf ą gqrw1 ,w2 r ; pf ą gqrw1 ,w2 s _ ppf ą gqrw1 ,w2 r ^ f pw2 q “ gpw2 qq .
(a2 ) Each such rewriting disrupts the structure of the overall formula,
which we can readily restore by bringing it again to disjunctive nor-
mal form δ1 _ δ2 _ ¨ ¨ ¨ _ δn (where n P t2, 4u) by means of the
distributive law
pα _ βq ^ γ Ø pα ^ γq _ pβ ^ γq ,
and then working on each δi separately in the sequel of this algo-
rithm.
(a3 ) Let w1 , w2 be numerical variables and f, g be functional variables.
In each δi where the literals pf ą gqsw1 ,w2 r , f pw1 q “ gpw1 q, and
f pw2 q “ gpw2 q occur together, when w1 ă w2 as ordered domain
variables and there are no domain variables between w1 and w2 , we
add the literals w1 ă w, w ă w2 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 ą tqs´8,w2 r ,
where f is a functional variable and t, w2 are numerical variables, as the
formula
pDrf s ą tqs´8,w1 s ^ pDrf s ą tqrw1 ,w2 r ^ w1 ă w2 ,
where w1 is the first 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 ,w2 s ^ 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,w2 r , pDrf s ă tqsw1 ,`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.:
(c1 ) we rewrite conjuncts of the forms
pDrf s ą tqsw1 ,w2 r , pDrf s ą tqrw1 ,w2 r , pDrf s ą tqsw1 ,w2 s ,
as equivalent disjunctions, for example:
pDrf s ą tqsw1 ,w2 s ; pDrf s ą tqrw1 ,w2 s _
ppDrf s ą tqsw1 ,w2 s ^ Drf spw1 q “ tq ;
(c2 ) we bring again the overall formula into disjunctive normal form tak-
ing the distributive law
pα _ βq ^ γ Ø pα ^ γq _ pβ ^ γq
into account.
(c3 ) If in a formula three literals pDrf s ą tqsw1 ,w2 r , Drf spw1 q “ t, and
Drtspw2 q “ t occur together, and are such that w1 ă w2 as ordered
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.
The same for pDrf s ă tqsw1 ,w2 r .
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 pred-
icates. 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 ,z2 s occurring in ϕ1 by the formula:
pz1 ď x ď z2 q ^ y1 “ f pxq ^ y2 “ gpxq ^ py1 “ y2 q.
(b) Replace any literal pf ą gqrw1 ,w2 s occurring in ϕ1 by the formula:
pw1 ď x ď w2 q ^ y1 “ f pxq ^ y2 “ gpxq ^ py1 ď y2 q,
In the same way we can remove literal on open and semi-open intervals.
(c) Replace any literal pDrf s “ tqrz1 ,z2 s (resp. ă, ď, ą, ě) occurring in ϕ1
by the formula:
pz1 ď x ď z2 q ^ y1 “ Drf spxq ^ py1 “ tq (resp. ă, ď, ą, ě ).
(d) Replace any literal Strict Up pf qrz1 ,z2 s (resp. Strict Down pf qrz1 ,z2 s )
occurring in ϕ1 by the formula:
Γ ^ y1 ě y2 presp. Γ ^ y1 ď y2 q ,
where
Γ :“ pz1 ď x1 ă x2 ď z2 q ^ y1 “ f px1 q ^ y2 “ f px2 q.
(e) Replace any literal Convexpf qrz1 ,z2 s (resp. Strict Convex pf qrz1 ,z2 s )
occurring in ϕ1 by the formula:
Γ ^ py2 ´ y1 qpx3 ´ x1 q ą px2 ´ x1 qpy3 ´ y1 q
presp. Γ ^ py2 ´ y1 qpx3 ´ x1 q ě px2 ´ x1 qpy3 ´ y1 qq ,
where
∆ :“ pz1 ď x1 ă x2 ă x3 ď z2 q,
Γ :“ ∆ ^ y1 “ f px1 q ^ y2 “ f px2 q ^ y3 “ f px3 q.
Literals of the forms Concavepf qrz1 ,z2 s , Strict Concave pf qrz1 ,z2 s 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 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 , tfj and add the literals yjf “ f pvj q and
tfj “ 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 “ tfj 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
tv1 , v2 , . . . , vr u of distinct domain variables of ϕ3 as follows:
$
& 1 if x “ ´8,
indpxq :“ l if x “ vl 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 γ0f , γrf and proceed as follows:
a) For each literal pf “ gqrz1 ,z2 s occurring in ϕ3 , add all literals yif “ yig , tfi “
yig whose subscript i satisfies indpz1 q ď i ď indpz2 q; moreover, if z1 “
´8 introduce the literal γ0f “ γ0g , and if z2 “ `8 introduce the literal
γrf “ γrg .
b) For each literal pf ą gqrw1 ,w2 s (resp. pf ą gqsw1 ,w2 r , pf ą gqrw1 ,w2 r ,
pf ą gqsw1 ,w2 s ) occurring in ϕ3 , add the following literal:
yif ą yig
for each indpw1 q ď i ď indpw2 q (resp. indpw1 q ă i ă indpw2 q, indpw1 q ď
i ă indpw2 q, indpw1 q ă i ď indpw2 q). Moreover if w1 ă w2 as domain
variables, in the case pf ą gqsw1 ,w2 r (resp. pf ą gqrw1 ,w2 r , pf ą gqsw1 ,w2 s )
add the following literals:
tfi ě tgi , tfj ď tgj presp. tfj ď tgj or tfi ě tgi q
with i “ indpw1 q and j “ indpw2 q.
c) For each literal pDrf s ’ yqrz1 ,z2 s occurring in ϕ3 , where ’P t“, ă, ą, ď, ěu,
add the following formulas:
f
yj`1 ´ yjf
tfi ’ y, ’ y,
vj`1 ´ vj
for each indpz1 q ď i, j ď indpz2 q, j “ indpz2 q, and if ’P tď, ěu add the
formulas: ˜ f ¸
yj`1 ´ yjf
“ y Ñ ptfj “ y ^ tfj`1 “ yq;
vj`1 ´ vj
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 ,w2 r (resp. pDrf s ’ yqsw1 ,w2 s , pDrf s ’
yqrw1 ,w2 r ) occurring in ϕ3 , where ’P t“, ă, ą, ď, ěu, add the formulas:
f
yj`1 ´ yjf
tfi ’ y, ’y
vj`1 ´ vj
for each indpw1 q ď j ă indpw2 q and for each indpw1 q ă i ă indpw2 q (resp.
indpw1 q ă i ď indpw2 q and indpw1 q ď i ă indpw2 q).
e) For each literal Strict Uppf qrz1 ,z2 s (resp. Strict Downpf qrz1 ,z2 s ) occurring
in ϕ3 , add the following literals:
tfi ě 0 presp. ďq, f
yj`1 ą yjf presp. ăq,
for each indpz1 q ď i, j ď indpz2 q, j “ indpz2 q; 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 ,z2 s (resp. Concavepf qrz1 ,z2 s ) occurring in ϕ3 ,
add the following formulas:
f
yi`1 ´ yif
tfi ď “ y ď tfi`1 presp. ěq,
vi`1 ´ vi
˜ f ¸
yi`1 ´ yif y f
´ y f
“ tfi _ i`1 i
“ tfi`1 Ñ ptfi “ tfi`1 q,
vi`1 ´ vi vi`1 ´ vi
for each indpz1 q ď i ă indpz2 q; moreover, if z1 “ ´8 introduce the
literal γ0f ď tf1 presp. ěq, and, if z2 “ `8, introduce the literal γrf ě
tfr presp. ďq.
g) For each literal Strict Convexpf qrz1 ,z2 s (resp. Strict Concavepf qrz1 ,z2 s ) oc-
curring in ϕ3 , add the following formulas:
f
yi`1 ´ yif
tfi ă ă tfi`1 presp. ąq,
vi`1 ´ vi
for each indpz1 q ď i ă indpz2 q; moreover, if z1 “ ´8, introduce the
literal γ0f ă tf0 presp. ąq, and, if z2 “ `8, introduce the literal γrf ą
tfr 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 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 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 for-
mulas 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 ex-
tend 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-defined starting from quadratic and exponential expressions.
These functions, and their derivatives, consistently express the properties of ϕ3
at points and real intervals.
5 An example
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 ą 0qsa,br Ñ Strict Uppf qra,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 ą 0qsa,br ^ Strict Uppf qra,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 ą 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 “ 0
“ ‰
_ pDrf s ą 0qsa,br ^ Drf spaq “ 0 ^ Drf spbq “ 0 ;
then we rearrange the overall formula into disjunctive normal form:
rpDrf s ą 0qra,bs ^ Strict Uppf qra,bs s
_ rpDrf s ą 0qra,br ^ Drf spbq “ 0 ^ Strict Uppf qra,bs s
(:)
_ rpDrf s ą 0qsa,bs ^ Drf spaq “ 0 ^ Strict Uppf qra,bs s
_ rpDrf s ą 0qsa,br ^ Drf spaq “ 0 ^ Drf spbq “ 0 ^ Strict Uppf qra,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 qra,bs , we can perform the rewriting
pDrf s ą 0qra,bs ^ Strict Uppf qra,bs ; pDrf s ą 0qra,bs ^ a ď x1 ă x2 ď b
^f px1 q “ y1 ^ f px2 q “ y2 ^ y2 ď y1 ,
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 ; v1 , x 1 ; v2 , x 2 ; v3 , b ; v4 , y 1 ; y 2 , y 2 ; y 3 ,
so that our formula ϕ2 becomes:
pDrf s ą 0qrv1 ,v4 s ^ v1 ď v2 ă v3 ď v4 ^ f pv2 q “ y2 ^ f pv3 q “ y3 ^ y3 ď y2 .
We can now evaluate the function f over the domain variables V “ tv1 , v2 , v3 , v4 u,
by adding the necessary literals:
ϕ3 :“ pDrf s ą 0qrv1 ,v4 s ^ v1 ď v2 ă v3 ď v4 ^ f pv2 q “ y2 ^ f pv3 q “ y3 ^ y3 ď y2
^f pv1 q “ y1f ^ f pv2 q “ y2f ^ f pv3 q “ y3f ^ f pv4 q “ y4f ^ y2 “ y2f ^ y3 “ y3f
^Drf spv1 q “ tf1 ^ Drf spv2 q “ tf2 ^ Drf spv3 q “ tf3 ^ Drf spv4 q “ tf4 .
ϕ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 “ y2f ^ y3 “ y3f
^ tf1 ą 0 ^ tf2 ą 0 ^ tf3 ą 0 ^ tf4 ą 0
y f ´y f y f ´y f y f ´y f
^ v22 ´v11 ą 0 ^ v33 ´v22 ą 0 ^ v44 ´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
y3f ´ y2f
v2 ă v3 ^ y2 “ y2f ^ y3 “ y3f ^ y3 ď y2 ^ ą 0,
v3 ´ v2
y f ´y f
whose constraints v2 ă v3 and y3f “ y3 ď y2 “ y2f yield that v33 ´v22 ď 0 .
By performing a similar analysis of the remaining three disjuncts of (:), one
proves the validity of our example.
Related works and complexity issues
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 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 [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 ex , sin x.
Conclusions and future work
This article has presented a decision algorithm for a fragment, RDF ` , of real
analysis, which extends the elementary algebra EAR of real numbers with vari-
ables designating functions of a real variable endowed with a continuous deriva-
tive. 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 s-
defined 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 ,w2 s .
Acknowledgments
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.
References
1. 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.
2. 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
3. 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.
4. 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.
5. 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.
6. 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.
7. 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.
8. Fisher M. J. and Rabin M. O., Super-exponential complexity of Presburger arith-
metic. Complexity and Computation, Vol. VII, SIAM-AMS, Philadelphia (1974),
2741.
9. Friedman H. and Seress À., Decidability in elementary analysis. I, Adv. Math. 76
(1989), no. 1, 94115.
10. Friedman H. and Seress À., Decidability in elementary analysis. II, Adv. Math. 79
(1990), no. 1, 1-17.
11. Grigoriev D., Complexity of deciding Tarski algebra, J. Symbolic Comput. 5 (1988),
65108.
12. 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.
291295.
13. Richardson D., Some undecidable problems involving elementary functions of a real
variable, J. Symbolic Logic 33 (1968), 514520.
14. 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)
15. 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.