=Paper=
{{Paper
|id=Vol-3733/paper15
|storemode=property
|title=Some Decidability Issues Concerning C^n Real Functions
|pdfUrl=https://ceur-ws.org/Vol-3733/paper15.pdf
|volume=Vol-3733
|authors=Gabriele Buriola,Domenico Cantone,Gianluca Cincotti,Eugenio Omodeo,Gaetano SpartΓ
|dblpUrl=https://dblp.org/rec/conf/cilc/BuriolaCCOS24
}}
==Some Decidability Issues Concerning C^n Real Functions==
https://ceur-ws.org/Vol-3733/paper15.pdf
Some decidability issues concerning πΆ π real functions
Gabriele Buriola1,* , Domenico Cantone2 , Gianluca Cincotti2 , Eugenio G. Omodeo3 and
Gaetano T. SpartΓ 4
1
Dept. of Computer Science, University of Verona, Italy
2
Dept. of Mathematics and Computer Science, University of Catania, Italy
3
Dept. of Mathematics, Informatics and Geosciences, University of Trieste, Italy
4
Pontifical Gregorian University, Rome, Italy
Abstract
This paper adapts preexisting decision algorithms to a family βπβ± = {RDFπ | π β N} of languages regarding
one-argument real functions; each RDF π is a quantifier-free theory about the differentiability class πΆ π , embodying
a fragment of Tarskian elementary algebra. The limits of decidability are also highlighted, by pointing out that
certain extensions of RDF π are undecidable. The possibility of extending RDF π into a language RDF β regarding
the class πΆ β , without disrupting decidability, is briefly discussed.
Two sorts of individual variables, namely real variables and function variables, are available in each RDF π .
The former are used to construct terms and formulas that involve basic arithmetic operations and comparison
relators between real terms, respectively. In contrast, terms designating functions involve function variables,
constructs for addition of functions and scalar multiplication, andβoutermostβπ-th order differentiation π·π [ ]
with π β©½ π. An array of predicate symbols designate various relationships between functions, as well as function
properties, that may hold over intervals of the real line; those are: function comparisons, strict and non-strict
monotonicity / convexity / concavity, comparisons between a function (or one of its derivatives) and a real term.
The decidability of RDF π relies, on the one hand, on Tarskiβs celebrated decision algorithm for the algebra
of real numbers, and, on the other hand, on reduction and interpolation techniques. An interpolation method,
specifically designed for the case π = 1, has been previously presented; another method, due to Carla Manni, can
be used when π = 2. For larger values of π, further research on interpolation is envisaged.
MS Classification 2020: 03B25, 26A06, 20F10.
Keywords
Decidable theories, Tarskiβs elementary algebra, Functions of a real variable
Introduction
This paper addresses the decision problem for a fragment of real analysis exploiting the renowned
decidability result for elementary real algebra due to Tarski [22, 23]. The Tarskian algebra being referred
to here is the first-order theory of the ordered field (R, 0, 1, +, Β·, =, β©½) of real numbers: within its
context, unlike with other first-order theories about numerical domainsβmost prominent, among those,
the DedekindβPeano integer arithmetic (see, e.g., [16, Chapter 3])β, an algorithm can establish whether
or not any given sentence is true. This motivates one in seeking extensions of elementary real algebra
where this decidability result is preserved: e.g., the decidability of Tarskian algebra enriched with the
exponential function resists, since long, as an unsolved issue [14]. We undertook years ago a systematic
study on enhancements of the Tarskian language, or fragments thereof, endowed with provisions
regarding real functions.
The language, dubbed RDF π , to be discussed in this paper is devoid of quantifiers but embodies,
in addition to the algebraic operators and relators, predicate symbols expressing strict and nonstrict
CILC 2024: 39th Italian Conference on Computational Logic, June 26β28, 2024, Rome, Italy
*
Corresponding author.
$ gabriele.buriola@univr.it (G. Buriola); domenico.cantone@unict.it (D. Cantone); cincotti@dmi.unict.it (G. Cincotti);
eomodeo@units.it (E. G. Omodeo); g.sparta@unigre.it (G. T. SpartΓ )
Β https://www.dmi.unict.it/cantone (D. Cantone); https://sites.units.it/eomodeo/index.html/ (E. G. Omodeo)
0000-0002-1612-0985 (G. Buriola); 0000-0002-1306-1166 (D. Cantone); 0000-0001-8460-1708 (G. Cincotti);
0000-0003-3917-1942 (E. G. Omodeo); 0000-0002-8993-5851 (G. T. SpartΓ )
Β© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
monotonicity, concavity, and convexity of πΆ π functions of one real variable, as well as strict and
non-strict comparisons β>β and ββ©Ύβ between functions, over bounded or unbounded intervals. Further
primitive constructs available in the language are: operators designating pointwise addition of functions,
multiplication of a function by a scalar, and differentiation operators (up to the π-th derivative).1 We
reduce the satisfiability problem regarding the formulas of RDF π to the truth problem for purely
existential sentences of the elementary algebra of reals; we can thus rely upon improved versions of
Tarskiβs original method.2
This paper is a sequel of [2] and [1]βhence, indirectly, of their antecedents [3, 5, 8]. As for semantics,
RDF π deals with functions endowed with continuous derivatives (up to the π-th order): in consequence
of this, a satisfiable RDF π formula might cease to be satisfiable in RDF π when π < π.3 Our present
language RDF π differs from the language RDF * studied in [1] in that its syntax is richer: now we
have a batch of differentiation constructs only one of which was available in RDF * ; this calls for an
enhancement of the decision algorithm, to wit, an enhanced reduction to Tarskian algebra.
Another novelty of the subject matter of this paper, with respect to its antecedents, is greater attention
bestowed to assessing where the boundary between decidable and undecidable fragments of analysis
precisely lies.
The ongoing is organized as follows. In Sec. 1, we introduce syntax and semantics of the language of
interest, and illustrate its expressive power through a gallery of small examples. Before providing the
detailed specification of our decision algorithm in Sec. 3, in Sec. 2 we exemplify its use by manually
working out an emulation of how it would process a specific, valid formula. Then Sec. 4 provides clues
on the correctness of the proposed decision algorithm, specifying the role of an ad hoc interpolation
method. Sec. 5 explores the other side of the problem in asking which further enrichments lead to
undecidability. To end, we outline possible connections with related work, and draw conclusions.4
1. The interpreted RDF π language
The augmented version RDF π of the theory RDF * of Reals with Differentiable Functions [1] is an
unquantified first-order theory dealing with reals and with real functions of class πΆ π of one real
variable, namely functions with continuous π-th derivative. The function symbols of RDF π designate
the basic operations of real arithmetic and pointwise addition, scalar multiplication, and differentiation
(up to the πth order) of functions. Its predicate symbols designate: comparisons between reals, pointwise
comparisons of functions; strict and non-strict monotonicity, convexity, and concavity; comparisons
between functions, and comparison between their derivatives (up to the π-th order), and real terms.
This section introduces the language underlying RDF π , explains the intended meanings of its con-
structs, and briefly illustrates its use.
Syntax and semantics
The language RDF π has two infinite supplies of individual variables, belonging to the respective sorts:
numerical variables π₯, π¦, π§, . . . and function variables π, π, β, . . . Numerical and function variables are
supposed to range, respectively, over the set R of real numbers and over the collection of functions
which interests us. Four constants are also available:
β’ the symbols 0 and 1;
β’ the distinguished symbols +β and ββ, occurring as ends of interval specifications (see below).
1
Usage of the differentiation operators π·π [ ] must be reasonably restrained, e.g., each of them can only appear as lead operator
in a function term g (which will then coincide with a term of the form π·[ f ]).
2
To make an example, polynomial methods for existential formulas with a fixed number of variables are available [19].
3
Partial evidence of this emerges from an example provided in [1, p. 128].
4
To ease the comparison between RDF π and similar previous theories, mainly RDF + and RDF * , the first three sections follow
much the same structure as the companion papers [2] and [1].
We next specify the syntax of terms, atoms, and formulas for RDF π .
Definition 1.1. Function terms, numerical terms, and interval specs are so defined:
a.1) Function variables are function terms;
a.2) if f and g are function terms, then f + g is a function term;
a.3) if f is a function term, then any βscalar multipleβ π f, with π a numerical term, is a function term.
b.1) Numerical variables and the constants 0, 1 are numerical terms;
b.2) if π and π‘ are numerical terms, the following also are numerical terms:
π +π‘, π βπ‘, and π Β· π‘ ;
b.3) if π‘ is a numerical term, πΌ a natural number between 1 and π, and f is a function term, then
f(π‘) and π·πΌ [f](π‘)
are numerical terms.5
c.1) An interval spec π΄ is an expression of any of the forms
[π1 , π2 ] , [π1 , π2 [ , ]π1 , π2 ] , and ]π1 , π2 [ ,
where π1 stands for either a numerical term or ββ, and π2 for either a numerical term or +β;
c.2) we dub the βextendedβ numerical terms π1 , π2 of such an π΄ the ends of π΄ . β£
Throughout, f and g stand for function terms, π and π‘ for numerical terms, and π΄ stands for an
interval spec.
Definition 1.2. An atom of RDF π is an expression of one of the forms
π = π‘, π > π‘, f(π ) = π‘, π·πΌ [f](π ) = π‘,
(f = g)π΄ , (f > g)π΄ , (f ββ· π‘)π΄ , (π·πΌ [f] ββ· π‘)π΄ ,
Up(f)π΄ , Down(f)π΄ , Convex(f)π΄ , Concave(f)π΄ ,
S_Up(f)π΄ , S_Down(f)π΄ , S_Convex(f)π΄ , S_Concave(f)π΄ ,
where ββ· β {=, <, >, β©½, β©Ύ } and πΌ is a natural number between 1 and π. β£
Definition 1.3. A formula of RDF π is any truth-functional combination of RDF π atoms. β£
For definiteness, we will construct the RDF π formulas from RDF π atoms by means of the usual
propositional connectives Β¬, β§, β¨, β, β.
The semantics of RDF π revolves around the designation rules listed in our next definition, with which
any truth-value assignment for the formulas of RDF π must comply.
Definition 1.4. An assignment for RDF π is a mapping π whose domain consists of all terms and
formulas of RDF π , satisfying the following conditions:
0. π 0 and π 1 are the real numbers 0 and 1.
5
As for the syntax, the availability of π·πΌ [ ] with πΌ > 1 is the only novelty with respect to [1]. We will signal in the body
of the decision algorithm which changes this enrichment entails. The true challenge, with this enrichment, is the need to
redesign the algorithm correctness proof.
1. For each numerical variable π₯, π π₯ is a real number.
2. For each function variable π , (π π ) is an everywhere defined real function of one real variable
of class πΆ π , i.e., with all the first π-th derivatives continuous.
(οΈ )οΈ
3. For each function term of the form f + g, the image π (f + g) (π) of any real number π is
(π f)(π) + (π g)(π).
4. For each function term )οΈ form π f, the function π (π f) is
(οΈ of the (οΈ defined )οΈto be ππ (π f).
Namely, the image π (π f) (π) of any real number π is ππ (π f)(π) .
5. For each numerical term of the form π‘1 β π‘2 with β β {+, β, Β·}, π (π‘1 β π‘2 ) is the real number
π π‘1 β π π‘2 .
6. For each numerical term of the form f(π‘), π (f(π‘)) is the real number (π f)(π π‘); for each
numerical term π·πΌ [f](π‘), π (π·πΌ [f](π‘)) is the real number π·πΌ [(π f)](π π‘), where π·πΌ [(π f)]
denotes the πΌ-th derivative of (π f).
7. For each interval specification π΄, π π΄ is an interval of R of the appropriate kind, whose endpoints
are the evaluations via π of the ends of π΄.6
For example, when π΄ = ]π‘1 , π‘2 ], then π π΄ = ]π π‘1 , π π‘2 ].
8. Truth values are assigned to formulas of RDF π according to the following rules, where π and π‘
stand for numerical terms and f, g for function terms:
a) π = π‘ (respectively π > π‘) is true iff π π = π π‘ (resp. π π > π π‘) holds;
b) (f = g)π΄ is true iff (π f)(π₯) = (π g)(π₯) holds for all π₯ in π π΄;
c) (f > g)π΄ is true iff (π f)(π₯) > (π g)(π₯) holds for all π₯ in π π΄;
d) (f ββ· π‘)π΄ , with ββ· β {=, <, >, β©½, β©Ύ}, is true iff (π f)(π₯) ββ· π π‘ holds for all π₯ in π π΄;
e) (π·[f] ββ· π‘)π΄ , with ββ· β {=, <, >, β©½, β©Ύ}, is true iff π·[(π f)](π₯) ββ· π π‘ holds for all π₯ in
π π΄;
f) Up(f)π΄ (respectively S_Up(f)π΄ ) is true iff (π f) is a monotone nondecreasing (resp. strictly
increasing) function in π π΄;
g) Convex(f)π΄ (respectively S_Convex(f)π΄ ) is true iff (π f) is a convex (resp. strictly convex)
function in π π΄;
h) the truth values of Down(f)π΄ , Concave(f)π΄ , S_Down(f)π΄ , and S_Concave(f)π΄ are defined
in close analogy with items f) and g);
i) the truth value which π assigns to a formula whose lead symbol is any of Β¬, β§, β¨, β, β
complies with the usual semantics of the propositional connectives.
An assignment π is said to model a set Ξ¦ of formulas when π π is true for every π in Ξ¦. β£
Note that RDF π coincides with RDF * (see [1]) when π = 1.
Definition 1.5 (Derived symbols). In light of the above semantics, we tacitly enrich our language,
much as in [2], with derived dyadic and triadic comparators involving numerical terms π‘1 , π‘2 , and π‘3 ;
namely π‘1 β π‘2 and π‘1 ββ· π‘2 /π‘3 , where β β {ΜΈ=, <, β©½, β©Ύ} and ββ· β {=, <, >, β©½, β©Ύ}.
Additional relators intermixing function terms and numerical terms, e.g., the construct
Linear(π )π΄ βDef Concave(π )π΄ β§ Convex(π )π΄ ,
can also be introduced by means of shortening definitions. β£
6
It goes without saying what is meant when π is undefined at either end of π΄ (actually, π (ββ) and π (+β) are undefined).
Some examples
Basic facts of real analysis stateable by means of RDF π formulas, with π > 1, are:
βΆ Linear(π )]ββ,+β[ β π·2 [π ] = 0 ]ββ,+β[ .
(οΈ )οΈ
A function π of class πΆ 2 is linear if and only if its second derivative is constantly null.
{οΈ [οΈ
βΆ (π < π₯ < π) β§ (S_Convex(π )[π,π₯] β§ S_Concave(π )[π₯,π] ) β¨
β π·2 [π ](π₯) = 0 .
]οΈ}οΈ
(S_Concave(π )[π,π₯] β§ S_Convex(π )[π₯,π] )
Let π₯ be an inflection point of a πΆ 2 function π , then the second derivative of π in π₯ is null.
[οΈ(οΈ ]οΈ
π·πβ1 [π ] = π¦ ]ββ,+β[ β π·π [π ] = 0 ]ββ,+β[ β§
)οΈ (οΈ )οΈ
βΆ
{οΈ(οΈ ]οΈ}οΈ
π·π [π ] = 0 ]ββ,+β[ β π·πβ1 [π ](π₯) = π¦ β π·πβ1 [π ] = π¦ ]ββ,+β[ .
)οΈ [οΈ (οΈ )οΈ
Let π be a function of class πΆ π , and π an integer, 0 < π β©½ π. Then the (π β 1)-st derivative of π
is constant if and only if the π-th derivative of π is null everywhere. (Note: π·πβ1 [π ] stands for π
when π = 1.)
{οΈ (οΈ )οΈ }οΈ
βΆ (π < π₯ < π) β§ π·[π ](π₯) = 0 β§ π·2 [π ] β©Ύ 0 [π,π] β§ π (π₯) = π¦ β (π β©Ύ π¦)[π,π] ;
{οΈ (οΈ )οΈ }οΈ
(π < π₯ < π) β§ π·[π ](π₯) = 0 β§ π·2 [π ] β©½ 0 [π,π] β§ π (π₯) = π¦ β (π β©½ π¦)[π,π] .
Let π be a function of class πΆ 2 , whose first derivative vanishes at some point π₯ and whose second
derivative is non-negative (resp., non-positive) all over a neighborhood [π, π] of that π₯. Then
π₯ is a relative minimum (resp., maximum) point for π . Note that an analogous conclusion can
be drawn about any function of class πΆ 2π+2 , whose first, second, . . . , and (2π + 1)-st derivative
vanish at some point π₯ and whose (2π + 2)-nd derivative is non-negative (resp., non-positive)
all over a neighborhood [π, π] of that π₯.
βΆ {οΈ
(π < [οΈπ₯ < π) β§ π·[π ](π₯) = 0 β§ π·2 [π ](π₯) ]οΈ= 0 β§
}οΈ
(οΈ 3 β
π· [π ] < 0 [π,π] β¨ π·3 [π ] > 0 [π,π]
)οΈ (οΈ )οΈ
{οΈ (οΈ )οΈ }οΈ
S_Convex(π )[π,π₯] β§ S_Concave(π )[π₯,π] β¨
(οΈ )οΈ .
S_Concave(π )[π,π₯] β§ S_Convex(π )[π₯,π]
Let π be a function of class πΆ 3 , whose first and second derivative vanish at some point π₯,
where the third derivative of π assumes a nonzero value. Then π₯ is an inflection point of π . (A
generalized variant of this statement is left to the insightful reader.)
2. The decision algorithm at work
Establishing that an RDF π formula π is valid is the same as establishing that its negation Β¬π is unsatis-
fiable; moreover, once Β¬π has been put in disjunctive normal form, satisfying it amounts to satisfying
one of its clauses. Thus, the core task regarding the decidability of RDF π is: how to determine whether
or not a given conjunction of RDF π literals (that is, RDF π atoms and negations thereof) is satisfiable?
Main steps of the decision algorithm
Via routinary flattening techniques, and in view of some basic properties of πΆ π functions, the said task
can be converted to the one of determining the satisfiability of an arbitrary conjunction π0 of atoms of
the forms
π₯=π¦ , π₯>π¦ , π§ =π₯Β·π¦ , π§ =π₯+π¦ ,
π¦ = π (π₯) , (π > π)π΄ , (π = π§ π)π΄ , (β = π + π)π΄ ,
π¦ = π·πΌ [π ](π₯) , (π·πΌ [π ] ββ· π§)π΄ , S_Up(π )π΄ , S_Down(π )π΄ ,
Convex(π )π΄ , Concave(π )π΄ , S_Convex(π )π΄ , S_Concave(π )π΄ ,
and of literals that are the complements of atoms of these forms involving an interval spec.7 As always,
π₯, π¦, π§ stand for numerical variables and π, π, β stand for function variables.
Through a possibly furcating process, π0 will undergo a series π0 β π1 β π2 β π3 β π4 = π ΜοΈ of
transformations, with no function variables occuring in the ending formula π; ΜοΈ thereby, the satisfiability
of π
ΜοΈ can be tested by means of Tarskiβs renowned decision algorithm [23, 9]. With a slight, harmless
ambiguity we dub βour algorithmβ at times our rewriting technique alone, and at times the entire
validity test consisting of it, preceded by various preparations (e.g., flattening), and supplemented with
Tarskiβs decision method.
The transformations ππβ1 β ππ (π = 1, 2, 3, 4) aim to the following purposes:
1. Behavior at the ends: For a thorough comparison between relevant values (e.g., the values of a
derivative at the endpoints of specific open or semi-open intervals), we must divide each literal
containing a function- or derivative-comparison into subcases, thus of either the form (π > π)π΄
or the form (π·πΌ [π ] ββ· π‘)π΄ , unless π΄ is a closed interval. By relying on function continuity, we
split each such literal into a finite disjunction covering all possible behaviors at ends. E.g.,
(π·πΌ [π ] < π‘)[π£,π€[ becomes (π·πΌ [π ] < π‘)[π£,π€] β¨ (π·πΌ [π ] < π‘)[π£,π€[ β§π·πΌ [π ](π€) = π‘ .
(οΈ )οΈ
2. Negative clause removal: Each negative literal with an interval specification is replaced by an
implicit existential assertion. E.g.,Β¬(π = π)[π£,π€] is replaced by π£ β©½ π₯ β©½ π€ β§ π (π₯) ΜΈ= π(π₯), where
π₯ is a new variable.
3. Explicit evaluation of function variables: With certain salient variables π£π , dubbed βdomain
variablesβ (e.g., the variable π£ in π (π£) = π¦), associate new variables π¦ππ , π‘1,π π,π
π , . . . , π‘π (one for each
function variable π ) subject to the constraints π¦ππ = π (π£π ), π‘1,π π,π
π = π·[π ](π£π ), . . . , π‘π = π·π [π ](π£π ).
2
E.g., if in RDF a formula involves one function variable π and three domain variables π£1 , π£2 , π£3
altogether, then this step brings 9 new numerical variables in, along with 9 equations:
π¦1π = π (π£1 ), π‘1,π
1 = π·[π ](π£1 ), π‘2,π 2
1 = π· [π ](π£1 ),
π¦2π = π (π£2 ), π‘1,π
2 = π·[π ](π£2 ), π‘2,π 2
2 = π· [π ](π£2 ),
π¦3π = π (π£3 ), π‘1,π
3 = π·[π ](π£3 ), π‘2,π 2
3 = π· [π ](π£3 ).
4. Elimination of function variables: Get rid of all literals involving function variables, whose
behaviours are already mimicked by the variables π¦ππ , π‘1,π π,π
π , . . . , π‘π introduced above. This elimi-
nation is obtained by introducing new number variables subject to suitable algebraic constraints.
π‘1,π 1,π
E.g., roughly speaking, (π·2 [π ] < π )[π£,π€] becomes π‘2,π 2,π
π£ < π β§ π‘π€ < π β§
π€ βπ‘π£
π€βπ£ < π .
A worked example
Our decision algorithm for RDF π is specified in full in Sec. 3; here, to convey a feel of how it works, we
consider a paradigmatic formula π and carry out one by one the key transformations leading from π to
a formula directly submittable to Tarskiβs algorithm for elementary real algebra.
Suppose that we want to establish whether the formula
β π·2 [π ](π₯) = 0,
{οΈ }οΈ
(π < π₯ < π) β§ S_Convex(π )[π,π₯] β§ S_Concave(π )[π₯,π]
7
Here again πΌ β {1, . . . , π}.
dubbed π in the ongoing, is true under every value assignment; equivalently, we can check whether
its negation Β¬π is unsatisfiable. Using classical properties of implication, the negation amounts to the
following formula π:
(π < π₯ < π) β§ S_Convex(π )[π,π₯] β§ S_Concave(π )[π₯,π] β§ π·2 [π ](π₯) ΜΈ= 0.
Then π undergoes the following transformations:
1. Behavior at the ends: Generally speaking, function-comparison literals of the form (π > π)π΄
must be bestowed special care, possibly leading to a subcase analysis. Since no such literal
appears in our π, this phase produces π1 := π .
2. Negative
(οΈ 2 clause removal:
)οΈ This phase removes negative literals with interval specifications,
(οΈ 2 )οΈsuch
as Β¬ π· [π ] = π¦ [π,π] , substituting them with suitable witnesses; for example, Β¬ π· [π ] = π¦ [π,π]
would be replaced by the following conjunction:
π β©½ π₯ β©½ π β§ π·2 [π ](π₯) = π β§ π ΜΈ= π¦.
Since the only negated literal in π, π·2 [π ](π₯) ΜΈ= 0, is pointwise, this phase produces π2 := π1 .
3. Explicit evaluation of function variables: This phase introduces a new variable to designate each
function-application term β(π£), where β stands for a function variable of π and π£ for one of its
so-called βdomainβ variables. To describe evaluation more transparently, let us do the renaming:
π β π£1 , π₯ β π£2 , π β π£3 . From the previous formula π2 we get the following π3 :
(π£1 < π£2 < π£3 ) β§ S_Convex(π )[π£1 ,π£2 ] β§ S_Concave(π )[π£2 ,π£3 ] β§ π·2 [π ](π£2 ) ΜΈ= 0 β§
π (π£1 ) = π¦1π β§ π (π£2 ) = π¦2π β§ π (π£3 ) = π¦3π β§
π· [π ](π£1 ) = π‘π1
1
β§ π· [π ](π£2 ) = π‘π2
1
β§ π· [π ](π£3 ) = π‘π3
1
β§
π·2 [π ](π£1 ) = π π1 β§ π·2 [π ](π£2 ) = π π2 β§ π·2 [π ](π£3 ) = π π3 β§ π π2 ΜΈ= 0.
4. Elimination of function variables: This final phase removes all literals still containing function
variables. We get rid of them by suitable replacements involving algebraic conditions, such as
the difference quotient for literals regarding derivatives. At the end we obtain an equisatisfiable
formula that can be tested for satisfiability by Tarskiβs algorithm.
From the previous formula π3 we get the following final formula π4 :
(π£1 < π£2 < π£3 ) β§ π π2 ΜΈ= 0 β§
π¦2π βπ¦1π
π‘π1 < π£2 βπ£1 < π‘π2 β§ π π1 β©Ύ 0 β§ π π2 β©Ύ 0 β§
π¦3π βπ¦2π
π‘π2 > π£3 βπ£2 > π‘π3 β§ π π2 β©½ 0 β§ π π3 β©½ 0.
In particular, the unsatisfiability of this last formula is given by the conjunction:
π π2 ΜΈ= 0 β§ π π2 β©Ύ 0 β§ π π2 β©½ 0.
3. The decision algorithm, in detail
When one deals with an unquantified language such as RDF π, which is closed with respect to proposi-
tional connectives, being able to determine algorithmically whether or not a formula is valid amounts
to establishing whether the negation thereof is satisfiable or unsatisfiable. }οΈ(E.g., ascertaining the validity
of the formula (π < π₯ < π) β§ S_Convex(π )[π,π₯] β§ S_Concave(π )[π₯,π] β π·2 [π ](π₯) = 0 amounts
{οΈ
to checking (π < π₯ < π) β§ S_Convex(π )[π,π₯] β§ S_Concave(π )[π₯,π] β§ π·2 [π ](π₯) ΜΈ= 0 for unsatisfiability .)
We prefer to address the satisfiability problem for RDF π here, so our algorithm is supposed to produce
a yes/no answer, where βyesβ means that π admits a model.
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 ππ , still devoid of quantifiers, each belonging to
elementary algebra of real numbers; this will be done so that π is satisfiable if and only if at least one of
the resulting ππ βs is satisfiable. Each resulting ππ can be tested via Tarskiβs decision algorithm.
First we discuss how to reduce our formula π to a particular format, called ordered form.
Normalization
Let T be an unquantified, possibly multi-sorted, first-order theory, endowed with: equality =, a
denumerable infinity of individual variables π₯1 , π₯2 , . . . , function symbols πΉ1 , πΉ2 , . . . , and predicate
symbols π1 , π2 , . . . .
Definition 3.1. A formula π of T is said to be flat if it is a conjunction of literals of the forms:
π₯ = π¦ , π₯ = πΉ (π₯1 , . . . , π₯π ) , π₯ ΜΈ= π¦ , π (π₯1 , . . . , π₯π ) , Β¬π (π₯1 , . . . , π₯π ) ,
with π₯, π¦, and the π₯π βs numerical variables, πΉ a function symbol and π a predicate symbol.
Let S be the class of all flat formulas of T ; the following holds:
Lemma 3.1. The decision problem for T , to wit, the problem of algorithmically determining whether or
not any given formula π in T is satisfiable, reduces to the analogous problem regarding S .
Proof. Each satisfiability algorithm for formulas in T clearly works also for formulas in the sublanguage
S of T . For the converse, suppose that an algorithmic satisfiability test for S is available, and let π
be any formula of T . Via routinary techniques, which in our case include rewriting rules such as
(β > π + π)π΄ β (β > π)π΄ β§ (π = π + π)]ββ,+β[ ,
(π·πΌ [π + π] = π¦)π΄ β (π·πΌ [π] = π¦)π΄ β§ (π = π + π)]ββ,+β[ ,
(S_Up(π + π))π΄ β (S_Up(π))π΄ β§ (π = π + π)]ββ,+β[ ,
(β‘)
(π + π = β + π)π΄ β (π = β + π)π΄ β§ (π = π + π)]ββ,+β[ ,
π (π (π₯)) = π¦ β π¦ = π (π§) β§ π§ = π (π₯) ,
(Up(π ))π΄ β (π·[π ] β©Ύ 0)π΄
(likewise, π·[π ](π·[π ](π₯)) = π¦ reduces to π¦ = π·[π ](π§) β§ π§ = π·[π ](π₯), etc.), one transforms π into an
equisatisfiable formula π such that
(1) every term occurring in π either is an individual variable or has the form πΉ (π₯1 , π₯2 , . . . , π₯π ),
where π₯1 , π₯2 , . . . , π₯π are individual variables and πΉ is a function symbol;
(2) every atom in π either has the form π₯ = π‘, where π₯ and π‘ are an individual variable and a term,
respectively, or has the form π (π₯1 , π₯2 , . . . , π₯π ), where π₯1 , π₯2 , . . . , π₯π are individual variables
and π is a predicate symbol.
Then one brings π to disjunctive normal form, thus obtaining a formula π1 β¨ Β· Β· Β· β¨ ππ
, where all
ππ βs are conjunctions. Additionally, we may assume that each ππ is flat, because any literal of type
Β¬ π₯ = πΉ (π¦1 , . . . , π¦π ) within it can be replaced by the conjunction π₯ ΜΈ= π§ β§ π§ = πΉ (π¦1 , . . . , π¦π ), where π§
is a brand new variable. Our claim follows, since
π is satisfiable β π is satisfiable β ππ is satisfiable for some π
and since all transformations used to obtain the conjunctions π1 , . . . , ππ
are effective.
We can now proceed to define an ordered form for RDF π formulas.
Definition 3.2. A domain variable in a formula π of RDF π is a numerical variable π₯ that occurs in π
either as the argument of a term of one of the forms π (π₯) and π·πΌ [π ](π₯), with π a function variable, or
as an end of some interval mentioned in π (as exemplified by Convex(π )[π₯,+β[ ).
Definition 3.3. An RDF π formula is said to be in ordered form if it is flat and has the form π β§
βοΈ πβ1
π=1 (π₯π < π₯π+1 ), where {π₯1 , . . . , π₯π } is the set of all distinct domain variables in π.
The family RDF ππππ of all ordered formulas of RDF π is a strict subset of RDF π ; notwithstanding:
Lemma 3.2. (Cf. [8, Lemma 1.4.3 on p.15]) RDF π is decidable if and only if RDF ππππ is decidable.
The algorithm
We describe next the decision algorithm for satisfiability of formulas of RDF π . In view of Lemma 3.2,
w.l.o.g. we assume that π is given in ordered form. Moreover, using new function variables β subject to
constraints of either the form (β = π + π)π΄ or the form (β = π§ π)π΄ , all literals, except those defining
these new ββs have been superseded by literals where no compound function terms occur. For example,
(π + π = 3 Β· π)[0,1] gets rewritten as (β1 = π + π)]ββ,+β[ β§ (β2 = 3 Β· π)]ββ,+β[ β§ (β1 = β2 )[0,1]
β further examples can be found in the rules in (β‘). Hence, in view of some basic properties of πΆ π
functions, the algorithm will only need to consider atomic formulas of the types
π₯=π¦ , π₯>π¦ , π§ =π₯Β·π¦ , π§ =π₯+π¦ ,
π¦ = π (π₯) , (π > π)π΄ , (π = π§ π)π΄ , (β = π + π)π΄ ,
π¦ = π·πΌ [π ](π₯) , (π·πΌ [π ] ββ· π§)π΄ , S_Up(π )π΄ , S_Down(π )π΄ ,
Convex(π )π΄ , Concave(π )π΄ , S_Convex(π )π΄ , S_Concave(π )π΄ ,
where ββ· β {=, <, >, β©½, β©Ύ }. (These types form a streamlined subset of the ones seen in Def. 1.2,
since they result from the flattening process mentioned earlier.) Moreover,
Remark 1. Leaving out of consideration literals of the types (π > π)π΄ , (π·πΌ [π ] > π¦)π΄ , (π·πΌ [π ] < π¦)π΄ ,
it suffices to take into account only closed intervals π΄; in fact, by continuity, the other properties are
valid in an open or semi-open interval if and only if they are valid in its closure, e.g., (π = π)]π€1 ,π€2 [
holds iff (π = π)[π€1 ,π€1 ] holds. β£
π
We can now focus on the algorithm which 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 a Tarskian formula, i.e., one containing only numerical variables, the arithmetical operators
+, Β· and the predicate symbols =, <.
As recalled in the introduction, there exists a decision algorithm for Tarskian formulas (cf. [23, 9]). A
decision algorithm for RDF π results from integrating Tarskiβs decision algorithm with the reduction
π β π we are about to present.
In the following, π€π denotes a numerical variable, π§π an βextendedβ numerical variable and πΌ a natural
number between 1 and π.
The series of transformations we need goes as follows:
1. π β π1 : behavior at the endpoints.
a) We rewrite each atom of the form (π > π)]ββ,π€2 [ , where π, π are function variables and
π€2 is a numerical variable, as the formula (π > π)]ββ,π€1 ] β§ (π > π)[π€1 ,π€2 [ β§ π€1 < π€2 ,
where π€1 is the first variable in the ordering of domain variables, if π€2 is preceded by at
least one such variable; otherwise, π€1 is a brand new domain variable.
We also perform the specular rewriting:
(π > π)]π€1 ,+β[ β (π > π)]π€1 ,π€2 ] β§ (π > π)[π€2 ,+β[ β§ π€1 < π€2 .
Thanks to the rewritings just made, every comparison between functions will refer either
to a closed interval or to a bounded interval. (The rewritings to be made at step c) will
serve a similar aim.)
b) Let π, π be real numbers such that π < π, and π, π be real continuous functions in the closed
interval [π, π]; then π > π holds in the open interval ]π, π[ if and only if either
i. π > π all over [π, π]; or
ii. π > π all over [π, π[, and π (π) = π(π); or
iii. π > π all over ]π, π], and π (π) = π(π); or
iv. π > π all over ]π, π[, and π (π) = π(π) β§ π (π) = π(π)
holds. By virtue of the previous equivalences, we perform the following actions:
b1 ) We rewrite a conjunct of this or of an alike form, namely an atom of one of the forms
(π > π)]π€1 ,π€2 [ , (π > π)[π€1 ,π€2 [ , (π > π)]π€1 ,π€2 ] ,
as an equivalent disjunction comprising 4 or just 2 alternatives; in particular:
(π > π)]π€1 ,π€2 [ β (π > π)[π€1 ,π€2 ] β¨
((π > π)[π€1 ,π€2 [ β§ π (π€2 ) = π(π€2 )) β¨
((π > π)]π€1 ,π€2 ] β§ π (π€1 ) = π(π€1 )) β¨
((π > π)]π€1 ,π€2 [ β§ π (π€1 ) = π(π€1 ) β§ π (π€2 ) = π(π€2 )) ,
(π > π)[π€1 ,π€2 [ β (π > π)[π€1 ,π€2 ] β¨ ((π > π)[π€1 ,π€2 [ β§ π (π€2 ) = π(π€2 )) ,
(π > π)]π€1 ,π€2 ] β (π > π)[π€1 ,π€2 ] β¨ ((π > π)]π€1 ,π€2 ] β§ π (π€1 ) = π(π€1 )) ,
b2 ) 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 β¨ Β· Β· Β· β¨ πΏπ (where
π β {2, 4}) by means of the distributive law (πΌ β¨ π½) β§ πΎ β (πΌ β§ πΎ) β¨ (π½ β§ πΎ) , and
then working on each πΏπ separately in the sequel of this algorithm.
b3 ) Let π€1 , π€2 be numerical variables and π, π be function variables. In each πΏπ where
the literals (π > π)]π€1 ,π€2 [ , π (π€1 ) = π(π€1 ), and π (π€2 ) = π(π€2 ) occur together, when
π€1 < π€2 as ordered domain variables and there are no domain variables between
π€1 and π€2 , we add the literals π€1 < π€, π€ < π€2 and π (π€) = π§, where π€ and π§ are
new numerical variables. Plainly, the resulting formula and the original one are
equisatisfiable.
c) We then rewrite each atom of the form (π·πΌ [π ] > π¦)]ββ,π€2 [ , where π is a function variable
and π¦, π€2 are numerical variables, as the formula (π·πΌ [π ] > π¦)]ββ,π€1 ] β§ (π·πΌ [π ] >
π¦)[π€1 ,π€2 [ β§ π€1 < π€2 , where π€1 is the first variable in the ordering of domain variables if
π€2 is preceded by at least one such variable; otherwise, π€1 is a brand new domain variable.
We also perform the specular rewriting:
(π·πΌ [π ] > π¦)]π€1 ,+β[ β (π·πΌ [π ] > π¦)]π€1 ,π€2 ] β§ (π·πΌ [π ] > π¦)[π€2 ,+β[ β§ π€1 < π€2 .
We handle similarly also the two cases (π·πΌ [π ] < π¦)]ββ,π€2 [ and (π·πΌ [π ] < π¦)]π€1 ,+β[ .
By these transformations we obtain an equisatisfiable formula.
d) Let π, π, and π‘ be real numbers and π a function, with π β πΆ π ([π, π]). Then π πΌ , the πΌ-th
derivative of π , is greater than π‘ in ]π, π[, π πΌ > π‘, if and only if one of the following holds:
i. π πΌ > π‘ in [π, π],
ii. π πΌ > π‘ in [π, π[ and π πΌ (π) = π‘,
iii. π πΌ > π‘ in ]π, π] and π πΌ (π) = π‘,
iv. π πΌ > π‘ in ]π, π[, π πΌ (π) = π‘ and π πΌ (π) = π‘.
The actions to be made are similar to the ones made under b):
d1 ) We rewrite conjuncts of the forms (π·πΌ [π ] > π¦)]π€1 ,π€2 [ , (π·πΌ [π ] > π¦)[π€1 ,π€2 [ , and
(π·πΌ [π ] > π¦)]π€1 ,π€2 ] , as equivalent disjunctions;(οΈfor example:
)οΈ(π· [π ] > π¦)]π€1 ,π€2 ] β (π· [π ] > π¦)[π€1 ,π€2 ] β¨ (π· [π ] > π¦)]π€1 ,π€2 ] β§ π· [π ](π€1 ) =
πΌ πΌ πΌ πΌ
π¦ .
We proceed similarly for (π·πΌ [π ] < π¦)]π€1 ,π€2 [ , (π·πΌ [π ] < π¦)[π€1 ,π€2 [ , (π·πΌ [π ] < π¦)]π€1 ,π€2 ] .
d2 ) We bring again the overall formula into disjunctive normal form, taking the distributive
law into account.
d3 ) If in a formula three literals (π·πΌ [π ] > π¦)]π€1 ,π€2 [ , π·πΌ [π ](π€1 ) = π¦, and π·πΌ [π ](π€2 ) = π¦
occur together, and they are such that π€1 < π€2 as ordered domain variables, and
there are no domain variables between π€1 and π€2 , we add the following literals:
π€1 < π€, π€ < π€2 and π (π€) = π§. We treat (π·πΌ [π ] < π¦)]π€1 ,π€2 [ likewise.
By applying rules a), b), c), and d) to a formula π in ordered form, we obtain a finite disjunction
of ππ ordered formulas such that π is satisfiable if and only if at least one of the ππ is satisfiable.
To each ππ we apply the rest of the algorithm.
2. π1 β π2 : negative-clause removal.
From π1 we construct an equisatisfiable formula π2 within which literals refferring to intervals
have no negative occurrences. The general idea applied in this step is to substitute every negative
clause involving a function symbol along with an interval spec with an implicit existential
assertion.
For the sake of simplicity, in the following:
β’ π₯, π₯1 , π₯2 , π₯3 , π¦1 , π¦2 , π¦3 will be numerical variables, new w.r.t. the formula considered;
β’ we use the notation π₯ βΌ π¦ as a shorthand for π₯ β©½ π¦ when π₯, π¦ are both numerical variables;
when either π₯ is ββ or π¦ is +β, π₯ βΌ π¦ stands for a true literal (e.g., 0 = 0).
a) Replace each literal Β¬(π = π§ π)[π§1 ,π§2 ] occurring in π1 by the formula (involving a new
function variable β) (π§1 βΌ π₯ βΌ π§2 )β§π¦1 = π (π₯)β§π¦2 = β(π₯)β§Β¬(π¦1 = π¦2 )β§(β = π§ π)[π§1 ,π§2 ] .
b) Replace each literal Β¬(β = π + π)[π§1 ,π§2 ] occurring in π1 by the formula (involving a new
function variable π) (π§1 βΌ π₯ βΌ π§2 )β§π¦1 = β(π₯)β§π¦2 = π(π₯)β§Β¬(π¦1 = π¦2 )β§(π = π +π)[π§1 ,π§2 ] .
c) Replace each literal Β¬(π > π)[π§1 ,π§2 ] occurring in π1 by the formula:
(π§1 βΌ π₯ βΌ π§2 ) β§ π¦1 = π (π₯) β§ π¦2 = π(π₯) β§ (π¦1 β©½ π¦2 ).
d) Replace each literal Β¬(π·πΌ [π ] ββ· π¦)[π§1 ,π§2 ] occurring in π1 by the formula:
(π§1 βΌ π₯ βΌ π§2 ) β§ π¦1 = π·πΌ [π ](π₯) β§ Β¬(π¦1 ββ· π¦) , where ββ·β {<, β©½, =, β©Ύ, >} .
e) Replace each literal Β¬S_Up (π )[π§1 ,π§2 ] (resp. Β¬ S_Down (π )[π§1 ,π§2 ] ) occurring in π1 by the
formula Ξ β§ π¦1 β©Ύ π¦2 (resp. Ξ β§ π¦1 β©½ π¦2 ) , where Ξ := (π§1 βΌ π₯1 < π₯2 βΌ π§2 ) β§ π¦1 =
π (π₯1 ) β§ π¦2 = π (π₯2 ).
f) Replace each literal Β¬ Convex(π )[π§1 ,π§2 ] (resp. Β¬ S_Convex (π )[π§1 ,π§2 ] ) occurring in π1 by
Ξβ§(π¦2 βπ¦1 )(π₯3 βπ₯1 ) > (π₯2 βπ₯1 )(π¦3 βπ¦1 ) (resp. Ξβ§(π¦2 βπ¦1 )(π₯3 βπ₯1 ) β©Ύ (π₯2 βπ₯1 )(π¦3 β
π¦1 )) , where Ξ := (π§1 βΌ π₯1 < π₯2 < π₯3 βΌ π§2 ) β§ π¦1 = π (π₯1 ) β§ π¦2 = π (π₯2 ) β§ π¦3 = π (π₯3 ).
Literals of the forms Β¬ Concave(π )[π§1 ,π§2 ] , Β¬ S_Concave (π )[π§1 ,π§2 ] are handled similarly.
Analogously, with only slight changes, we can remove literals about open and semi-open intervals:
e.g., Β¬(π > π)]π€1 ,π€2 ] becomes (π€1 < π₯ β©½ π€2 ) β§ π¦1 = π (π₯) β§ π¦2 = π(π₯) β§ (π¦1 β©½ π¦2 ).
Equisatisfiability of the formulas π1 and π2 is straightforward to prove. According to Lemma 3.1
and Lemma 3.2, we can transform π2 , to obtain an equivalent formula in ordered form with
domain variables π£1 , π£2 , . . . , π£π .
3. π2 β π3 : explicit evaluation of function variables.
This step is preparatory to the elimination of the functional clauses, by explicit evaluation of
function variables over domain variables. For each such variable π£π and for every function
variable π occurring in π2 , introduce π + 1 new numerical variables π¦ππ , π‘1,π π,π
π , . . . , π‘π and add
the literals π¦ππ = π (π£π ), π‘1,π π,π
π = π·[π ](π£π ), . . . , π‘π = π·π [π ](π£π ) to π2 . Moreover, for each literal
π₯ = π (π£π ) already occurring in π2 , add the literal π₯ = π¦ππ into π3 ; and similarly, for each literal of
type π₯ = π·πΌ [π ](π£π ) already occurring in π2 , insert the literal π₯ = π‘πΌ,π
π into π3 .
The formula π3 resulting from these insertions and the original π2 are clearly equisatisfiable.
4. π3 β π4 : elimination of function variables.
As a final step, we get rid of all literals containing function variables.
Define the index function πππ : π βͺ {ββ, +β} β {1, 2, . . . , π} over the set {π£1 , π£2 , . . . , π£π } of
distinct domain variables of π3 as β§ follows:
β¨ 1 if π₯ = ββ,
πππ(π₯) := π if π₯ = π£π for some π β {1, 2, . . . , π},
π if π₯ = +β.
β©
For each function symbol π occurring in π3 , introduce new numerical variables π0π , πππ , πΎ01,π, . . . , πΎ0π,π,
πΎπ1,π, . . . , πΎππ,π, and proceed as follows:
a) For each literal (π = π)[π§1 ,π§2 ] occurring in π3 , add all literals π¦ππ = π¦ππ , π‘1,ππ = π‘1,π
π ,...,
π,π π,π
π‘π = π‘π whose subscript π satisfies πππ(π§1 ) β©½ π β©½ πππ(π§2 ); moreover, if π§1 = ββ
introduce the literals πΎ01,π = πΎ01,π , . . . , πΎ0π,π = πΎ0π,π , and if π§2 = +β introduce the literals
πΎπ1,π = πΎπ1,π , . . . , πΎππ,π = πΎππ,π .
b) For each literal (π = π§ π)[π§1 ,π§2 ] occurring in π3 , add all literals π¦ππ = π§ π¦ππ , π‘1,π π =
1,π π,π π,π
π§ π‘π , . . . , π‘π = π§ π‘π , whose subscript π satisfies πππ(π§1 ) β©½ π β©½πππ(π§2 ); moreover, if
π§1 = ββ then introduce the literals πΎ01,π = π§ πΎ01,π , . . . , πΎ0π,π = π§ πΎ0π,π , and if π§2 = +β
then introduce the literals πΎπ1,π = π§ πΎπ1,π , . . . , πΎππ,π = π§ πΎππ,π .
c) For each literal (β = π + π)[π§1 ,π§2 ] occurring in π3 , add all literals π¦πβ = π¦ππ + π¦ππ , π‘1,β π =
1,π 1,π π,β π,π π,π
π‘π +π‘π , . . . , π‘π = π‘π +π‘π whose subscript π satisfies πππ(π§1 ) β©½ π β©½ πππ(π§2 ); moreover,
if π§1 = ββ then introduce the literals πΎ01,β = πΎ01,π + πΎ01,π , . . . , πΎ0π,β = πΎ0π,π + πΎ0π,π , and if
π§2 = +β then introduce the literals πΎπ1,β = πΎπ1,π + πΎπ1,π , . . . , πΎππ,β = πΎππ,π + πΎππ,π .
d) For literals of type (π > π)π΄ , we consider separately bounded and unbounded intervals:
d1 ) For each literal (π > π)[π€1 ,π€2 ] (resp. (π > π)]π€1 ,π€2 [ , (π > π)[π€1 ,π€2 [ , (π > π)]π€1 ,π€2 ] ) oc-
curring in π3 , add the literals π¦ππ > π¦ππ with πππ(π€1 ) β©½ π β©½ πππ(π€2 ) (resp. πππ(π€1 ) <
π < πππ(π€2 ), πππ(π€1 ) β©½ π < πππ(π€2 ), and πππ(π€1 ) < π β©½ πππ(π€2 )). Moreover, if
π€1 < π€2 as domain variables, in the case (π > π)]π€1 ,π€2 [ (resp. (π > π)[π€1 ,π€2 [ , (π >
π)]π€1 ,π€2 ] ) also add the literals π‘1,π 1,π 1,π 1,π 1,π
πππ(π€1 ) β©Ύ π‘πππ(π€1 ) , π‘πππ(π€2 ) β©½ π‘πππ(π€2 ) (resp. π‘πππ(π€2 ) β©½
π‘1,π 1,π 1,π
πππ(π€2 ) or π‘πππ(π€1 ) β©Ύ π‘πππ(π€1 ) ).
d2 ) For each literal (π > π)]ββ,+β[ (resp. (π > π)]ββ,π€1 ] , (π > π)[π€1 ,+β[ ) occurring in
π3 , add the literal π¦ππ > π¦ππ with 1 β©½ π β©½ π (resp. 1 β©½ π β©½ πππ(π€1 ), πππ(π€1 ) β©½ π β©½ π), and
the literals π0π β©Ύ π0π , πππ β©Ύ πππ (resp. π0π β©Ύ π0π or πππ β©Ύ πππ ).
e) For literals of type (π·πΌ [π ] ββ· π¦)π΄ , we consider separately closed and unclosed interval
specifications:8
e1 ) For each literal (π·[π ]πΌ ββ· π¦)[π§1 ,π§2 ] occurring in π3 , where ββ·β {=, <, >, β©½, β©Ύ}, add
the following formulas:
π‘πΌβ1,π βπ‘πΌβ1,π
π‘πΌ,π
π ββ· π¦, π+1π£π+1 βπ£
π
π
ββ· π¦,
for πππ(π§1 ) β©½ π β©½ πππ(π§2 ) and πππ(π§1 ) β©½ π < πππ(π§2 ), and if ββ·β {β©½, β©Ύ} add the
implication: (οΈ )οΈ
π‘πΌβ1,π
π+1 βπ‘π
πΌβ1,π
π£π+1 βπ£π =π¦ β (π‘πΌ,π
π = π¦ β§ π‘πΌ,π
π+1 = π¦);
moreover, if π§1 = ββ, introduce the literal πΎ0πΌ,π ββ· π¦, and if π§2 = +β, introduce the
literal πΎππΌ,π ββ· π¦.
e2 ) For each literal (π·πΌ [π ] ββ· π¦)]π€1 ,π€2 [ (resp. (π·πΌ [π ] ββ· π¦)]π€1 ,π€2 ] , (π·πΌ [π ] ββ· π¦)[π€1 ,π€2 [ )
occurring in π3 , where ββ·β {=, <, >, β©½, β©Ύ}, add the formulas:
8
The treatment of these literals, novel with respect to [1], is a straightforward refinement of the corresponding algorithm step
[1, step 4.e)].
π‘πΌβ1,π βπ‘πΌβ1,π
π‘πΌ,π
π ββ· π¦, π+1π£π+1 βπ£
π
π
ββ· π¦ ,
for πππ(π€1 ) β©½ π < πππ(π€2 ) and πππ(π€1 ) < π < πππ(π€2 ) (resp. πππ(π€1 ) < π β©½ πππ(π€2 )
and πππ(π€1 ) β©½ π < πππ(π€2 )).
f) For each literal S_Up(π )[π§1 ,π§2 ] (resp. S_Down(π )[π§1 ,π§2 ] ) occurring in π3 , add the literals
π‘1,π
π β©Ύ 0 (resp. β©½), π¦π+1 π
> π¦ππ (resp. <),
for πππ(π§1 ) β©½ π β©½ πππ(π§2 ) and πππ(π§1 ) β©½ π < πππ(π§2 ); moreover, if π§1 = ββ, introduce
the literal πΎ01,π > 0 (resp. <) and, if π§2 = +β, introduce the formula πΎπ1,π > 0 (resp. <).
g) For each literal Convex(π )[π§1 ,π§2 ] (resp. Concave(π )[π§1 ,π§2 ] ) occurring in π3 , add:
π¦π βπ¦ π
π‘1,π β©½ π£π+1 π
β©½ π‘1,π
π+1 (resp. β©Ύ), )οΈπ‘2,π β©Ύ 0 (resp. β©½)
(οΈ π π π
π+1 βπ£π
π π
π
π¦π+1 βπ¦π π¦π+1 βπ¦π
(οΈ )οΈ
1,π 1,π 1,π 1,π
π£π+1 βπ£π = π‘π β¨ π£π+1 βπ£π = π‘π+1 β π‘ π = π‘π+1 ,
for each πππ(π§1 ) β©½ π < πππ(π§2 ); moreover, if π§1 = ββ, introduce the literal πΎ01,π β©½ π‘1,π
1
(resp. β©Ύ), and, if π§2 = +β, introduce the literal πΎπ1,π β©Ύ π‘1,π
π (resp. β©½).
h) For each literal S_Convex(π )[π§1 ,π§2 ] (resp. S_Concave(π )[π§1 ,π§2 ] ) occurring in π3 , add:
π¦π βπ¦ π
π‘1,π
π < π£π+1 π
π+1 βπ£π
< π‘1,π 2,π
π+1 (resp. >), π‘π β©Ύ 0 (resp. β©½)
for πππ(π§1 ) β©½ π < πππ(π§2 ); moreover, if π§1 = ββ, introduce the literal πΎ01,π < π‘1,π
1 (resp. >),
and, if π§2 = +β, introduce the literal πΎπ1,π > π‘1,π
π (resp. <).
i) If there are literals involving variables of type π, i.e., literals of the form πππ β©Ύ πππ with
π β {0, π} and π, π function variables, perform the following steps:
i. for each variable πππ , add the formula β1 β©½ πππ β©½ +1, with π β {0, π};
ii. if both literals πππ β©Ύ πππ and πππ β©Ύ ππβ occur in π4 , add literals πππ β©Ύ ππβ and π¦ππ > π¦πβ ,
with π β {0, π};
iii. if literals π0π β©Ύ π0π , πΎ01,π β΅ π and πΎ01,π β΄ π occur together, with β΅ β {β©Ύ, >, =} and
β΄ β {β©½, <, =}, add literal π β©½ π; specularly, in the case πππ β©Ύ πππ , πΎπ1,π β΄ π and
πΎπ1,π β΅ π, add the literal π β©Ύ π.
j) Remove all literals that involve function variables.
The formula π4 resulting at the end involves only numerical variables, hence it can be decided by means
of Tarskiβs method.
4. Remarks on the correctness of the algorithm
Proving the correctness of the algorithm amounts to showing that each one of the (terminating)
transformations π β π1 , π1 β π2 , π2 β π3 , π3 β π4 is satisfiability preserving. As for the first three
transformations (behavior at the endpoints, negative-clause removal, explicit evaluation of function
variables), this emerges as a rather straightforward fact.
We must focus on the equisatisfiability of the formulas π3 and π4 , because the transformation
π3 β π4 is less transparent than the previous ones: we are, in fact, comparing a formula whose
predicates regard the behavior of functions in real intervals with another one, which only involves
relations between numerical variables. Let us sketch the idea behind the proof, which as usual consists
of two parts: soundness and completeness. Recall that π4 is obtained from π3 by adding some formulas
that involve only numerical variables and removing all predicates that refer to function 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 the properties of the functions in π3 at specific points
in real intervals.
Completeness: Conversely, if there exists a model for π4 , it should be possible to extend it to π3 by
interpreting the function variables with suitable interpolating functions. Thus, showing the correctness
of the fourth transformation calls for an ad hoc interpolation method, which we have produced explicitly
for the case π = 1 in [1]; when π = 2, we could borrow an interpolation method due to Manni [15];
when π > 2, we hope for, and remain in debt with the reader of, a proof of existence of the suitable
interpolating function.
Completeness for RDF 2 , a birdβs-eye view
The completeness for RDF 2 relies on the interpolation method developed by Manni [15] which is a shape-
preserving πΆ 2 interpolation method. This means that, given a grid of real numbers π£1 < π£2 < Β· Β· Β· < π£π
and real values π¦π , π‘π , π π with π β {1, . . . , π}, Manniβs method builds a πΆ 2 real function π such that, for
all π β {1, . . . , π}:
π (π£π ) = π¦π , π β² (π£π ) = π‘π and π β²β² (π£π ) = π π . (1)
Moreover, Manniβs method has three properties relevant for our aims:
1. It preserves the βgeometric propertiesβ [10] of the given data π£π , π¦π , π‘π , π π ; e.g, if the data are
increasing, π¦π β©½ π¦π+1 and π‘π β©Ύ 0 for all π, so will be the interpolating function.
2. The interpolation of a sum of data is the sum of the two interpolations; namely given two series
of values π¦ππ , π‘ππ , π ππ and π¦ππ , π‘ππ , π ππ over the same grid π£1 < π£2 < Β· Β· Β· < π£π with, respectively,
two interpolating functions π and π, then π + π is the interpolating function for the values
π¦ππ + π¦ππ , π‘ππ + π‘ππ , π ππ + π ππ .
3. Beside the given data π£π , π¦π , π‘π , π π , the interpolating function π built by the method depends on a
shrinking parameter π and we will use the notation ππ to emphasize the dependency from this
parameter π. As π tends toward 0, the function ππ tends to the piece-wise linear interpolation
passing through the points (π£1 , π¦1 ), . . . , (π£π , π¦π ); more precisely limπβ0 ||ππ β π||β = 0 where
||ππ β π||β = supπ£1 β©½π₯β©½π£π |ππ (π₯) β π(π₯)| and π is the piece-wise linear interpolation passing
through the points (π£π , π¦π ).9
Roughly speaking, having Manniβs method at our disposal the completeness proof goes as follows.
Given a numerical model π for π4 , i.e., a set of real values which satisfies all the algebraic constraints
in π4 , we use Manniβs method to build from π a functional model β± for π3 , namely a set of real
functions interpreting all the function variables of π3 and satisfying all the function requirements.
More precisely, let π£Β― denote the interpretation π π£ of the numerical variable π£ under the model M.
Given a function variable π in π3 , we apply Manniβs method to the values π£Β―π , π¦Β―ππ , Β―π‘ππ and Β―π ππ to obtain a
πΆ 2 function πΒ― which will be the interpretation of π . By (1), πΒ― satisfies all point-wise conditions such
as π·[π ](π£3 ) = π‘π3 . The remaining part consists in proving that, for π small enough, the interpolating
function πΒ― π satisfies also all the other possible atomic formulas, e.g. (π·[π ] > π )[π£π ,π£π [ ; this part heavily
relies on the three interpolation properties previously exposed.
5. The threshold of undecidability
Tarski himself showed that decidability of his full elementary algebra of real numbers [23] would be
disrupted if its language were enriched with a periodic real function, e.g., sin π₯. Richardson proved
in [20] the undecidability of the existential theory of reals extended with the numbers log 2 and π,
and with the functions ππ₯ , sin π₯; Richardsonβs results have been subsequently improved by Caviness
[7], Wang [24] and Laczkovich [13]. More precisely: Caviness removed the use of ππ₯ and ln 2; Wang
extended Cavinessβ result from undecidability for comparison with 0, namely of type π΄(π₯) < 0, to
π₯βπ£π
9
Over the interval [π£π , π£π+1 ], π is defined as π(π₯) := π¦π + π£π+1 βπ£π
Β· (π¦π+1 β π¦π ).
undecidability for equality to 0, i.e., π΄(π₯) = 0; Laczkovich removed the need of π and reduced the use
of function composition.
In consequence of Laczkovichβs result and of our reduction of RDF π to Tarskian algebra, any extension
π
(οΈ RDF
of enabling us to express sin π₯ turns out to be undecidable. For example, an atomic formula
2
)οΈ
π· [π ] = π π΄ for equality between a second derivative and a function would allow one to specify
π = sin π₯ through the differential characterization:
π (0) = 0 β§ π·1 [π ](0) = 1 β§ (π·2 [π ] = (οΈ βπ )]ββ,+β[
)οΈ .
Thus, for π β©Ύ 2, the introduction of atomic formulas of type π·2 [π ] = π π΄ would make RDF π unde-
cidable. Establishing whether or not an analogous extension of RDF 1 is decidable is harder. As far as
we now, having comparison between first derivatives and functions does not allow one to define sin π₯;
however, it enables the definition of ππ₯ via
π (0) = 1 β§ (π·1 [π ] = π )]ββ,+β[ ,
but, since even the decidability of Tarskian algebra extended with the exponential function is still an
open
(οΈ 1 problem)οΈ [14], we cannot judge whether such an enrichment, i.e., function-derivative comparison
π· [π ] = π π΄ , would disrupt the decidability of RDF 1 .
Conclusions
Applications
The decidability result presented in this paper is not merely of theoretical interest, but can be seen
as a contribution to the automated reasoning field; as a matter of fact RMCF + , one of the decision
algorithms from which it originates, was discussed in the monograph [21], which is a companion of the
proof-verification system ΓtnaNova: if it were implemented inside such a system, a decision algorithm
akin to it could play the role of a sophisticated and specialized inference mechanism.10 Regrettably,
though, the worst-case algorithmic complexity of the known algorithms concerned with real functions,
in their present forms, is not encouraging [3]; discouragement can be alleviated by considerations about
the behaviour in typical cases, as discussed in the same context (cf. [3, pp. 775β776]).
Envisaged applications of a system such as ΓtnaNova regard proof checking as well as program-
correctness verification; parts of it specialized on real algebra and analysis might also assist in formal
hardware validation and in the study of hybrid systems.
Given the enduring popularity of resolution, research on decision algorithmsβwhether focusing on
fragments of mathematical theories or logical calculi, or addressing entire theoriesβhas only sporadically
influenced the field of automated deduction. Notable exceptions include the influential papers by Nelson-
Oppen [17, 18]. These works are significant not because they add to the inventory of decidable theories,
but because they address the integration of decision algorithms. In this regard, their impact and long-
term influence are comparable to that of the DPLL algorithm, which, besides being directly applicable
as a test for propositional logic, often serves as a crucial and ubiquitous inference mechanism.
Related and future work
This article has presented a decision algorithm for a fragment RDF π of real analysis, which extends
the unquantified part of Tarskiβs elementary algebra EAR of real numbers with variables designating
functions of a real variable endowed with continuous derivatives up the π-th order.
The decidability of the theory RDF π is a follow-up of a series of previous results, regarding the
theories RMCF, RMCF + , RDF, RDF + and RDF * [5, 3, 8, 4, 2, 1]. A general survey on those results, save
the last two, can be found in [6], where other decidability results on real analysis are also treated, in
particular the FS theory [11, 12].
It is hoped that decision methods regarding differentiable functions from Rπ to Rπ are amenable to
the approach discussed above: an encouraging indication in this direction comes from [5, Sec. 4] which,
10
Actually, less specialized than it may seem at first glance: as shown in [5, Sec. 5], a decision algorithm conceived for
real numbers and univariate real functions could be exploited to reason about a totally ordered set (π, <) and monotone
functions from π to π.
however, deals with continuous function (with no concern about differentiability).
A decidability problem that seems worth being investigated regards the theory RDF β , whose set of
formulas is the union of all RDF π formulas with π β N (hence we have a differentiation operator π·π [ ]
for every natural number π); the intended semantics will refer to the real functions of class πΆ β . The
decision algorithm will proceed in full analogy with the one of each RDF π ; the correctness proof seems
more challenging, though, because the interpolating method needs to accommodate an arbitrarily high
number of derivative constraints. Thus far, we have no evidence in favor or against the existence of the
sought πΆ β interpolant.
References
[1] Buriola G., Cantone D., Cincotti G., Omodeo E.G., SpartΓ G.T., A decidable theory treating addition of differentiable real
functions. Theoretical Computer Science, 940:124-148, 2023.
[2] Buriola G., Cantone D., Cincotti G., Omodeo E.G., SpartΓ G.T., A decidable theory of differentiable functions with
convexities and concavities on real intervals. In Francesco Calimeri, Simona Perri, and Ester Zumpano, eds, Proceedings
of the 35th Italian Conference on Computational Logic - CILC 2020, Rende, Italy, October 13-15, 2020, CEUR Workshop
Proceedings, 2710:231-247. CEUR-WS.org, 2020.
[3] Cantone D., Cincotti G., Gallo G., Decision algorithms for fragments of real analysis. I. Continuous functions with strict
convexity and concavity predicates. J. Symb. Comput., 41(7):763-789, 2006.
[4] 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
[5] 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.
[6] 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.
[7] Caviness B.F., On Canonical Forms and Simplification, Journal of the ACM 17 (2) (1970), 385β396.
[8] 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.
[9] Collins G., Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Second GI Conference
on Automata Theory and Formal Languages, LNCS Vol.33, Springer-Verlag, Berlin, 1975.
[10] Goodman T.N.T., Shape preserving interpolation by curves, Algorithms for Approximation IV, editors Levesley J., Anderson
I. and Mason J., 2002.
[11] Friedman H. and Seress Γ., Decidability in elementary analysis. I, Adv. Math. 76 (1989), no. 1, 94β115.
[12] Friedman H. and Seress Γ., Decidability in elementary analysis. II, Adv. Math. 79 (1990), no. 1, 1β17.
[13] Laczkovich M., The removal of π from some undecidable problems involving elementary functions, Proceedings of the
AMS 131 (7) (2002), 2235β2240.
[14] Macintyre, A. and Wilkie, A.J., On the Decidability of the Real Exponential Field, Kreiseliana. About and Around Georg
Kreisel, (1996), 441β467.
[15] Manni C., On Shape Preserving πΆ 2 Hermite Interpolation, BIT Numerical Mathematics, vol. 41 (2001), pp. 127β148.
[16] Mendelson, E., Introduction to Mathematical Logic, CRC Press, Discrete Mathematics and Its Applications, 2015 ISBN
9781482237788.
[17] Nelson, G. and Oppen, D.C., Simplification by cooperating decision procedures, ACM Trans. on Programming Languages
and Systems 1(2) (1979), 245β257.
[18] Nelson, G. and Oppen, D.C., Fast decision procedures based on congruence closure, Journal of the ACM 27(2) (1980),
356β364.
[19] Renegar J., A faster PSPACE algorithm for deciding the existential theory of the reals, 29th Annual Symposium on
Foundations of Computer Science (FOCS 1988, Los Angeles, Ca., USA), IEEE Computer Society Press, Los Alamitos
(1988), pp. 291β295.
[20] Richardson D., Some undecidable problems involving elementary functions of a real variable, J. Symbolic Logic 33 (1968),
514β520.
[21] Schwartz J.T., Cantone D., Omodeo E.G., Computational logic and set theory: Applying formalized logic to analysis.
Springer-Verlag, 2011. ISBN 978-0-85729-807-2. Foreword by M. Davis.
[22] 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 submitted for publication in 1940)
[23] 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
published by the University of California Press, Berkeley and Los Angeles, CA, 1951, iii+63 pp.
[24] Wang P.S., The undecidability of the existence of zeros of real elementary functions, Journal of the ACM 21 (4) (1974),
586-589.