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 diferentiability 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 diferentiation [ ] 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.
This paper addresses the decision problem for a fragment of real analysis exploiting the renowned
decidability result for elementary real algebra due to Tarski [
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 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 diferentiation 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
This paper is a sequel of [
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 Diferentiable Functions [
This section introduces the language underlying RDF , explains the intended meanings of its constructs, and briefly illustrates its use.
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).
1Usage of the diferentiation 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 ]).
2To make an example, polynomial methods for existential formulas with a fixed number of variables are available [
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: b.3) if is a numerical term, a natural number between 1 and , and f is a function term, then + , − ,
and · ; 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.
= , (f = g),
Up(f), S_Up(f),
> , (f > g),
Down(f), S_Down(f), f() = , (f ◁▷ ),
Convex(f), S_Convex(f), [f]() = , ( [f] ◁▷ ),
Concave(f), S_Concave(f), where ◁▷ ∈ {=, <, >, ⩽, ⩾ } and is a natural number between 1 and . Definition 1.3.
For definiteness, we will construct the 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.
5As for the syntax, the availability of [ ] with > 1 is the only novelty with respect to [
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 if = (resp. > ) holds; b) (f = g) is true if ( f)() = ( g)() holds for all in ; c) (f > g) is true if ( f)() > ( g)() holds for all in ; d) (f ◁▷ ), with ◁▷ ∈ {=, <, >, ⩽, ⩾}, is true if ( f)() ◁▷ holds for all in ; e) ([f] ◁▷ ), with ◁▷ ∈ {=, <, >, ⩽, ⩾}, is true if [( f)]() ◁▷ holds for all in ; f) Up(f) (respectively S_Up(f)) is true if ( f) is a monotone nondecreasing (resp. strictly increasing) function in ;
function in ;
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 [
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. ⊣ 6It goes without saying what is meant when is undefined at either end of (actually, (−∞ ) and (+∞) are undefined).
▶ Linear( )]−∞ ,+∞[ ↔ ︀( 2[ ] = 0)︀ ]−∞ ,+∞[ .
▶ {︀ ( < < ) ∧ ︀[ (S_Convex( )[,] ∧ S_Concave( )[,]) ∨ (S_Concave( )[,] ∧ S_Convex( )[,])
→ ︀]} 2[ ]() = 0 .
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 ( − is constant if and only if the -th derivative of is null everywhere. (Note: − 1[ ] stands for 1)-st derivative of 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.)
¬ Establishing that an RDF formula is valid is the same as establishing that its negation ¬ is unsatisifable; 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?
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
= , = () , = [ ]() ,
Convex( ) ,
> , ( > ) , ( [ ] ◁▷ ) , Concave( ) ,
= · , ( = ) ,
S_Up( ) , S_Convex( ) ,
= + , (ℎ = + ) ,
S_Down( ) , 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 [
The transformations − 1 ↝ ( = 1, 2, 3, 4) aim to the following purposes:
is a new variable. 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 3. Explicit evaluation of function variables: With certain salient variables , dubbed “domain variables” (e.g., the variable in () = ), associate new variables function variable ) subject to the constraints = ( ), 1, = [ ]( ), . . . , , = [ ]( ).
E.g., if in RDF 2 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, , . . . , , (one for each 1 = (1), 2 = (2), 3 = (3), 1, = [ ](1), 1 1, = [ ](2), 2 1, = [ ](3), 3 2, = 2[ ](1), 1 2, = 2[ ](2), 2 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 elimination is obtained by introducing new number variables subject to suitable algebraic constraints. E.g., roughly speaking, (2[ ] < )[,] becomes 2, < ∧ 2, < ∧ 1, − − 1,
< .
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 ︀{ ( < < ) ∧ S_Convex( )[,] ∧ S_Concave( )[,] ︀} → 2[ ]() = 0, 7Here again ∈ {1, . . . , }. following formula : 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 ( < < ) ∧
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 clause removal: This phase removes negative literals with interval specifications, such as ¬ (︀ 2[ ] = )︀ [,], substituting them with suitable witnesses; for example, ¬ (︀ 2[ ] = )︀ [,] 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
∧ 1[ ](1) = 1 ∧ 2[ ](1) = 1 ∧
(2) = 2 1[ ](2) = 2 2[ ](2) = 2 ∧ ∧ ∧
(3) = 3 1[ ](3) = 3 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 diference 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) 1 < 22 −− 11 <
2 2 > 33 −− 22 > 3 ∧ ∧ ∧ 2 ̸= 0 1 ⩾ 0 2 ⩽ 0 ∧ ∧ ∧ 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 propositional connectives, being able to determine algorithmically whether or not a formula is valid amounts to establishing whether the negation thereof is satisfiable or unsatisfiable . (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.
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.
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 efective.
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 ⋀︀=−11( < +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.
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 · )[
= , = () , = [ ]() ,
Convex( ) ,
> , ( > ) , ( [ ] ◁▷ ) , Concave( ) ,
= · , ( = ) ,
S_Up( ) , S_Convex( ) ,
= + , (ℎ = + ) ,
S_Down( ) , 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 sufices 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 if ( = )[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. [
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:
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] ↝ ↝ ↝ ( > )[1,2] ∨ (( > )[1,2[ ∧ (2) = (2)) ∨ (( > )]1,2] ∧ (1) = (1)) ∨ (( > )]1,2[ ∧ (1) = (1) ∧ (2) = (2)) , ( > )[1,2] ∨ (( > )[1,2[ ∧ (2) = (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.
From 1 we construct an equisatisfiable formula 2 within which literals referring 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, . . . , .
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.
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 1 ,, . . . ,
,, and proceed as follows: a) For each literal ( = )[1,2] occurring in 3, add all literals = , 1, = 1 ,, . . . , 1 , = 1 ,, . . . ,
, = ,. , = , whose subscript satisfies introduce the literals 01, = 01,, . . . , 0 (1) ⩽ ⩽ (2); moreover, if 1 = −∞ , = 0,, and if 2 = +∞ introduce the literals then introduce the literals 1, = 1,, . . . , , = ,. b) For each literal ( = )[1,2] occurring in 3, add all literals = , 1, = 1 = −∞ 1 ,, . . . , , = ,, whose subscript satisfies (1) ⩽ ⩽ (2); moreover, if then introduce the literals 01, = 01,, . . . , 0 , = 0,, and if 2 = +∞ c) For each literal (ℎ = + )[1,2] occurring in 3, add all literals ℎ = + , 1,ℎ = 1, +1 ,, . . . , ,ℎ = , + , whose subscript satisfies (1) ⩽ ⩽ (2); moreover, 2 = +∞ then introduce the literals 1 ,ℎ = 1 , + 1 ,, . . . , ,ℎ = , + ,. if 1 = −∞ then introduce the literals 01,ℎ = 01, + 01,, . . . , 0 ,ℎ = 0 , + 0 ,, and if 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]) occurring 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, 1, 1, (1) ⩾ (1), (2) ⩽ (2) (resp. 1, 1, (2) ⩽ )]1,2]) also add the literals 1, 1, (2) or 1,(1) ⩾ (1)). specifications: 8 the literals 0 ⩾ 0, ⩾ (resp. 0 ⩾
0 or ⩾ ). d2) For each literal ( > )]−∞ ,+∞[ (resp. ( > )]−∞ ,1], ( > )[1,+∞[) occurring in 3, add the literal >
with 1 ⩽ ⩽ (resp. 1 ⩽ ⩽ (1), (1) ⩽ ⩽ ), and e) For literals of type ( [ ] ◁▷ ), we consider separately closed and unclosed interval the following formulas: e1) For each literal ([ ] ◁▷ )[1,2] occurring in 3, where ◁▷∈ {=, <, >, ⩽, ⩾}, add , ◁▷ , +−11, − − 1, +1− ◁▷ , implication: for (1) ⩽ ⩽ (2) and (1) ⩽ < (2), and if ◁▷∈ {⩽, ⩾} add the ︂( +−11, − − 1, +1− = ︂) → ( ,
, = ∧ +1 = ); literal
, ◁▷ .
moreover, if 1 = −∞ , introduce the literal 0, ◁▷ , and if 2 = +∞, introduce the
e2) For each literal ( [ ] ◁▷ )]1,2[ (resp. ( [ ] ◁▷ )]1,2], ( [ ] ◁▷ )[1,2[)
occurring in 3, where ◁▷∈ {=, <, >, ⩽, ⩾}, add the formulas:
8The treatment of these literals, novel with respect to [
, ◁▷ , +−11,+ −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 +,1 (resp. ⩾), 2 , ⩾ 0 (resp. ⩽) ︂( ++11− − = 1 , ∨ ++11− − = 1 +,1︂) → ︁( 1 , = 1 +,1)︁ , for each (1) ⩽ < (2); moreover, if 1 = −∞ , introduce the literal 01, ⩽ 11, (resp. ⩾), and, if 2 = +∞, introduce the literal 1, (resp. ⩽).
1, ⩾ h) For each literal S_Convex( )[1,2] (resp. S_Concave( )[1,2]) occurring in 3, add: 1, < +1−
+1− < 1 +,1 (resp. >), 2 , ⩾ 0 (resp. ⩽) for (1) ⩽ < (2); moreover, if 1 = −∞ , introduce the literal 01, < 11, (resp. >), and, if 2 = +∞, introduce the literal 1, (resp. <).
1, > 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 ⊴1 ∈, ⊵{⩽,,<a,d=d}th,ea dlidtelriatelral ⩾⩽. ; specularly, in the case ⩾ , 1, ⊴ and 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 [
Completeness for RDF 2, a bird’s-eye view
The completeness for RDF 2 relies on the interpolation method developed by Manni [
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 [
In consequence of Laczkovich’s result and of our reduction of RDF to Tarskian algebra, any extension of RDF 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 (0) = 0 ∧ 1[ ](0) = 1 ∧ (2[ ] = − )]−∞ Thus, for ⩾ 2, the introduction of atomic formulas of type (︀ 2[ ] = ︀) would make RDF undecidable. 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 problem [
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 [
Æ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 [
Envisaged applications of a system such as ÆtnaNova regard proof checking as well as programcorrectness 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
NelsonOppen [
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 * [
It is hoped that decision methods regarding diferentiable functions from
the approach discussed above: an encouraging indication in this direction comes from [5, Sec. 4] which, 10Actually, 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 diferentiability).
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 diferentiation 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.