=Paper=
{{Paper
|id=Vol-1269/paper46
|storemode=property
|title=A Function Elimination Method for Checking Satisfiability of Arithmetical Logics
|pdfUrl=https://ceur-ws.org/Vol-1269/paper46.pdf
|volume=Vol-1269
|dblpUrl=https://dblp.org/rec/conf/csp/CastiglioniLT14
}}
==A Function Elimination Method for Checking Satisfiability of Arithmetical Logics==
https://ceur-ws.org/Vol-1269/paper46.pdf
A Function Elimination Method for Checking
Satisfiability of Arithmetical Logics
Valentina Castiglioni, Ruggero Lanotte, and Simone Tini
Dipartimento di Scienza e Alta Tecnologia, Università dell’Insubria
Abstract. We study function elimination for Arithmetical Logics. We
propose a method allowing substitution of functions appearing in a given
formula with functions with less arity. We prove the correctness of the
method and we use it to show the decidability of the satisfiability problem
for two classes of formulae allowing linear and polynomial terms.
1 Introduction
A branch of First Order Logics are Arithmetical Logics. Arithmetical Logics
consider quantified formulae where variables are either reals or integers, and
where functions in {+, ·} and relations in {<, =, >, ≤, ≥} are used.
The satisfiability problem deals with the existence of a valuation for vari-
ables, functions and predicates s.t. a given formula is true under that valuation.
This problem is in general undecidable if one considers polynomial formulae on
integer variables (see [23]). Different classes are considered to avoid such diffi-
culty, and several techniques can be used to prove decidability (see [4]). One of
these techniques is based on the quantifier elimination approach. Given a formula
with a quantified variable, the quantifier elimination deals with the problem of
finding an equivalent formula without quantifiers.
The results of this paper are the following ones: we prove that quantifier
elimination for formulae with functions cannot exist; we introduce a technique
that permits to decrease the arity of a certain function; we use the technique
proposed to prove the decidability of the satisfiability problem for two subclasses
of formulae in the set of formulae with prefixes in (∃∗ ∀)∗ . The two classes (the
first one allowing real polynomial terms and the second one mixed linear terms)
are sufficient to describe the theories of sets and strings.
The paper is organized as follows: in Section 2 we review some base notions
and results on Arithmetical Logics. In Section 3 we show the function elimination
method and the two decidable classes are defined in Section 4. In Section 5 we
use our method to model sets and in Section 6 we discuss related works and
draw some conclusions.
2 Background
Let us assume a set of function symbols F ranged over by a, b, . . . together with
an arity mapping ar : F → IN. If ar(a) = 0 then a is called a real variable. We
will usually use x, y, . . . to denote real variables.
A valuation over F is a mapping v : F → (IRIN → IR) that assigns a function
v(a) : IRar(a) → IR to each function symbol a. Notice that v(x) is a constant for
each variable x. The set of all valuations over F is denoted by V. For a valuation
v ∈ V, a function symbol a and a function f : IRar(a) → IR, we denote with
v[f /a] the valuation s.t. v[f /a](a) = f and v[f /a](b) = v(b) for all b 6= a.
Definition 1. The set T of polynomial terms with rational coefficients, ranged
over by τ , is defined inductively by:
τ ::= q | q · a(τ1 , . . . , τar(a) ) | τ1 + τ2 | τ1 · τ2
where q ∈ Q and a ∈ F . The terms in T generated without using the multiplica-
tion τ1 · τ2 are called linear terms.
When we use real variables in terms, we usually write x for x(). For instance,
we will write x + 3 for x() + 3. We assume a function ID : T → 2F that, applied
to a term τ ∈ T , returns the set of the function symbols appearing in τ .
Example 1. Let ar(a) = ar(b) = 1 and x, y be two real variables. If τ1 is the
term 94 ·x·(b(x+a(y 2 )))4 and τ2 is 9+3·x+ 23 ·y +b(a(y)) then τ1 is a polynomial
term, τ2 is a linear term, and ID(τ1 ) = ID(τ2 ) = {x, y, a, b}.
For a term τ ∈ T and a valuation v ∈ V, we denote with [τ ]v the value of τ
under the valuation v, more precisely:
[q]v = q
[q · a(τ1 , . . . , τar(a) )]v = q · v(a)([τ1 ]v , . . . , [τar(a) ]v )
[τ1 + τ2 ]v = [τ1 ]v + [τ2 ]v
[τ1 · τ2 ]v = [τ1 ]v · [τ2 ]v
Definition 2. The set Φ of quantified formulae over T is defined inductively
by:
φ ::= τ ∼ τ 0 | int(τ ) | ∃a . φ0 | ¬φ1 | φ1 ∨ φ2
where τ, τ 0 ∈ T , ∼∈ {<, ≤, =, ≥, >} and a ∈ F . Conjunction, implication and
universal quantification can be easily derived. We say that φ is linear iff for each
τ ∼ τ 0 and int(τ ) appearing in φ, it holds that τ, τ 0 are linear terms.
For a quantified formula φ ∈ Φ and a valuation v ∈ V, we write v |= φ if v
satisfies φ. The relation |= is defined as follows:
v |= τ ∼ τ 0 iff [τ ]v ∼ [τ 0 ]v
v |= int(τ ) iff [τ ]v ∈ ZZ
v |= ∃a.φ0 iff there exists a f : IRar(a) → IR s.t. v[f /a] |= φ0
v |= ¬φ1 iff v 6|= φ1 (namely v |= φ does not hold)
v |= φ1 ∨ φ2 iff v |= φ1 or v |= φ2 .
For a formula φ ∈ Φ, we denote with JφK the set of valuations in V that
satisfy φ, formally JφK = {v ∈ V | v |= φ}. Two formulae φ1 and φ2 are equivalent
iff Jφ1 K = Jφ2 K. We denote with true the formula 0 = 0 and with false the
formula ¬true. So, true, false are in Φ. Notice that JfalseK = ∅ and JtrueK = V.
Moreover, with Free(φ) we denote the set of real variables and functions symbols
non-quantified in φ, and with Bnd(φ) we denote the set of real variables and
functions symbols quantified in φ. We assume, without loss of generality, that
the sets Free(φ) and Bnd(φ) are always disjoint.
Example 2. Let x, y be two real variables, and a, b be two function symbols with
ar(a) = 1 and ar(b) = 2. We give some properties that can be expressed in Φ:
– The function b( , 1) is the square of a( ): ∀x.a(x) · a(x) = b(x, 1).
– The function a assumes only integer values: ∀x.int(a(x)).
– The function a reaches x: ∃y.a(y) = x.
– The minimum of a is in position x: ∀y.a(y) ≥ a(x).
– The function a is binary: ∀x.a(x) = 0 ∨ a(x) = 1.
– The function a is monotone: ∀x, y.x ≤ y ⇒ a(x) ≤ a(y).
Given two terms τ1 , τ2 ∈ T , with φ[τ1 := τ2 ] we denote the formula obtained
by replacing all occurrences of τ1 in φ with τ2 . Moreover, if a is a function symbol
in F , let App(a, φ) denote the set of terms a(τ1 , . . . , τar(a) ) appearing in φ.
Definition 3. E = {∃a. | a ∈ F }∗ is called the set of existential quantification
prefixes, F = {∀a. | a ∈ F }∗ is called the set of universal quantification prefixes,
and Q = {∃a., ∀a. | a ∈ F }∗ is called the set of quantification prefixes.
For instance, ∃a.∃b. is in E and ∃a.∀b. is in Q. From now on, without loss of
generality we consider formulae of the form Q.φ where Q ∈ Q, and Bnd(φ) = ∅.
Definition 4. A quantified formula φ ∈ Φ is satisfiable iff JφK 6= ∅. The satis-
fiability problem for φ ∈ Φ consists in answering if φ is satisfiable.
The satisfiability problem is in general undecidable if one considers quantified
polynomial formulae on integer variables (see [23]). Different classes of formulae
have been considered to avoid such a difficulty. For quantified linear formulae
on real and integer variables (without function symbols a with ar(a) > 0), the
satisfiability problem is decidable (see [34]). In fact, in this case quantifiers can
be eliminated through quantifier elimination, which consists in transforming a
formula ∃x.φ where Bnd(φ) = ∅ into an equivalent formula φ0 s.t. Bnd(φ0 ) = ∅.
For instance, ∃x.5 < x∧x < y can be transformed into the equivalent formula 5 <
y. In general, quantifier elimination does not hold if one considers also functions
(see [7] and [16] for example). The problem is that the variables appearing in the
scope of some functions cannot be eliminated. The following proposition states
that quantifier elimination cannot work, in general, for the formulae in Φ.
Proposition 1. Let φ be the formula ∀x . 0 ≤ x < y ⇒ a(x) = 0. There is no
formula φ0 ∈ Φ with Bnd(φ0 ) = ∅ equivalent to φ.
For a formula ∃a.φ with Bnd(φ) = ∅, we say that a is an uninterpretated
function. The satisfiability of such a formula is decidable. In fact, by following
[30], one can get a formula φ0 equivalent to ∃a.φ by substituting each occurrence
a(τ1 , . . . , τar(a) ) in φ with a real variable x, provided φ is updated in a suitable
way that, however, does not require to introduce any function with arity > 0.
Then, since the φ0 so obtained does not contain functions with arity > 0, its
satisfiability is decidable according to [34]. For instance, ∃a.a(4) ≤ a(k) can be
turned into ∃x.∃y.x ≤ y ∧ ((4 = k) ⇒ (x = y)). The challenge is to extend this
method to formulae not in the form ∃a.φ with Bnd(φ) = ∅. This is immediate for
formulae of the form ∃a.∃x.φ with Bnd(φ) = ∅, since such a formula is equivalent
to ∃x.∃a.φ, which can be transformed to ∃x.φ0 , to which quantifier elimination
applies. The difficulty is in the formulae of the form ∃a.∀x.φ and ∀a.∃x.φ. In
next section we consider the case ∃a.∀x.φ since ∀a.∃x.φ = ¬∃a.∀x.¬φ.
3 The function elimination method
In this section we give two results showing under which circumstances a function
in a quantified formula in Φ can be replaced by a function with less arguments.
If, by iteratively applying these substitutions, we transform each function into a
real variable, then satisfiability follows from results in [32] and [34].
First of all we investigate when all occurrences in a formula φ of a function
a can be substituted by occurrences of a function b that applies to a subset of
the arguments of a (Theorem 1 below).
Definition 5. A term τ ∈ T is determined by a real variable x iff [τ ]v 6= [τ ]v0
for all valuations v, v 0 ∈ V s.t. v(x) 6= v 0 (x), and v(y) = v 0 (y) for all y 6= x.
For instance, the terms x3 +a(z)·z 2 and 3·x+2 are determined by x, whereas
the terms x2 and a(x) are not determined by x.
Proposition 2. It is decidable to check whether τ is determined by x.
Definition 6. Let a ∈ F , S ⊆ {1, . . . , ar(a)} with S 6= ∅, x be a real variable
and φ ∈ Φ. We say that a is S-fixed on x in φ iff:
– for each i 6∈ S and a(τ1 , . . . , τar(a) ) ∈ App(a, φ), it holds that x 6∈ ID(τi );
– for each i ∈ S, there exists a term τ̂i determined by x s.t. ID(τ̂i ) ⊆ Free(φ) ∪
{x} and, for all a(τ1 , . . . , τar(a) ) ∈ App(a, φ), it holds that τi = τ̂i .
Informally, a is S-fixed on x in φ iff for all terms of the form a(τ1 , . . . , τar(a) )
appearing in φ, the real variable x appears in all and only the terms τi with
i ∈ S and, for each i ∈ S, the respective term τi is unique and determined by
x. This implies that, for each c, c0 ∈ IR with c 6= c0 , the values of the argument
terms τi with i ∈ S to which a is applied in φ[x := c] are different from those to
which a is applied in φ[x := c0 ]. Hence, φ[x := c] and φ[x := c0 ] can be considered
separately if one wants to delete the quantified function symbol a.
Example 3. We consider the following running example. Let φr be the formula
∃b.∀x.∀y.∃a.∀z.a(z + b(y 3 , x + 5)) = b(y 3 , b(y 3 , 3)) ∧ a(0) = k where x, y, z and
k are real variables, and a, b are functions s.t. ar(a) = 1 and ar(b) = 2. We
have that b is {1}-fixed on y in φr . Then, b is not S-fixed on x in φr , for any S.
Finally, a is not {1}-fixed on any variable in φr .
If a is S-fixed on x in φ with {1, . . . , ar(a)} \ S = {i1 , . . . , im }, and a0 is a
function symbol s.t. ar(a0 ) = m, then let Sub(a, a0 , S, φ) denote the formula
(φ){[a(τ1 , . . . , τar(a) ) := a0 (τi1 , . . . , τim )] | a(τ1 , . . . , τar(a) ) ∈ App(a, φ)}
resulting from the substitution in φ of each occurrence of a with a0 applied to
the argument terms of a that are not in positions in S.
Theorem 1. Assume a formula φ ∈ Φ, a function symbol a ∈ F , a real variable
x and a set S ⊆ {1, . . . , ar(a)}. If a is S-fixed on x in φ, then
∃a.∀x.φ is equivalent to ∀x.∃a0 .Sub(a, a0 , S, φ).
Example 4. Consider the formula φr in Ex. 3. By applying Th. 1 to b we get the
equivalent formula φ0r : ∀y.∃b0 .∀x.∃a.∀z.a(z +b0 (x + 5)) = b0 (b0 (3)) ∧ a(0) = k.
Now we investigate when a given term a(τ1 , . . . , τar(a) ) in App(a, φ) can be
replaced by a term a0 (τ1 , . . . , τj−1 , τj+1 , . . . τar(a) ). The idea is to generalize to
arbitrary functions the technique proposed in [30] to replace uninterpreted func-
tions with functions with less arguments.
Let φ ∈ Φ and a ∈ F . With EQ(a, φ) we denote the formula
^ ^
τi = τi0 ⇒ a(τ1 , . . . , τar(a) ) = a(τ10 , . . . , τar(a)
0
)
a(τ1 ,...,τar(a) ) i∈[1,ar(a)]
a(τ10 ,...,τar(a)
0 )
∈ App(a, φ)
expressing that if two arbitrary occurrences of a in φ are applied to argument
terms with the same values, then the resulting values are equal.
Example 5. Let φ0r be as the formula in Ex. 4. Then EQ(b0 , φ0r ) is equivalent to
(x + 5 = b0 (3)) ⇒ b0 (x + 5) = b0 (b0 (3)) ∧ (x + 5 = 3) ⇒ b0 (x + 5) = b0 (3) ∧ (b0 (3) =
3) ⇒ b0 (b0 (3)) = b0 (3).
In [2] it is proved that the formula ∃f.∀y.P (y, f (y)), with P a predicate, is
equivalent to ∀y.∃x.P (y, x). We apply the same strategy to formulae in Φ.
Theorem 2. Let φ0 ∈ Φ be the formula ∃a.Q.φ with Bnd(φ) = ∅, and let
a(τ1 , . . . , τar(a) ) be a term in App(a, φ) s.t. for some 1 ≤ j ≤ ar(a) it holds
ID(τj ) ⊆ Free(φ0 ). Then φ0 is equivalent to the formula
∃a.∃a0 .Q.(φ ∧ EQ(a, φ))[a(τ1 , . . . , τar(a) ) := a0 (τ1 , . . . , τj−1 , τj+1 , . . . , τar(a) )].
Example 6. Let us consider the formula φ0r in Ex. 4. By applying Th. 2 to term
b0 (3) ∈ App(b0 , φ0r ) we obtain the equivalent formula
∀y.∃b0 .∃w.∀x.∃a.∀z.a(z + b0 (x + 5)) = b0 (w) ∧ a(0) = k ∧ (w = 3 ⇒ b0 (w) =
w) ∧ (x + 5 = w ⇒ b0 (x + 5) = b0 (w)) ∧ (x + 5 = 3 ⇒ b0 (x + 5) = w).
Now, by applying Th. 2 to term b0 (w), we get the equivalent formula
∀y.∃b0 .∃w.∃t.∀x.∃a.∀z.a(z + b0 (x + 5)) = t ∧ a(0) = k ∧ (w = 3 ⇒ t =
w) ∧ (x + 5 = w ⇒ b0 (x + 5) = t) ∧ (x + 5 = 3 ⇒ b0 (x + 5) = w).
We can now apply Th. 1 to function symbol b0 , which is now {1}-fixed on x,
thus obtaining the equivalent formula
∀y.∃w.∃t.∀x.∃s.∃a.∀z.a(z + s) = t ∧ a(0) = k ∧ (w = 3 ⇒ t = w) ∧ (x + 5 =
w ⇒ s = t) ∧ (x + 5 = 3 ⇒ s = w).
By applying Th. 2 to term a(0) we get the equivalent formula
∀y.∃w.∃t.∀x.∃s.∃a.∃a0 .∀z.a(z + s) = t ∧ a0 = k ∧ (w = 3 ⇒ t = w) ∧ (x + 5 =
w ⇒ s = t) ∧ (x + 5 = 3 ⇒ s = w) ∧ (z + s = 0 ⇒ a(z + s) = a0 ).
By applying Th. 1 to function symbol a, which is {1}-fixed on z, we obtain the
equivalent formula
∀y.∃w.∃t.∀x.∃s.∃a0 .∀z.∃a00 .a00 = t ∧ a0 = k ∧ (w = 3 ⇒ t = w) ∧ (x + 5 =
w ⇒ s = t) ∧ (x + 5 = 3 ⇒ s = w) ∧ (z + s = 0 ⇒ a00 = a0 ).
which has no function with arity > 0. Therefore its satisfiability is decidable.
The formula above is equivalent to the original formula φr in Ex. 3.
The following result is a generalization of Th. 2.
Corollary 1. Let φ0 ∈ Φ be the formula ∃a.Q.φ with Bnd(φ) = ∅, and let
a(τ1 , . . . , τar(a) ) be a term in App(a, φ) s.t. for some j1 , . . . , jk in 1, . . . , ar(a),
ID(τjh ) ⊆ Free(φ0 ) for each h = 1, . . . , k. Then φ0 is equivalent to the formula
∃a.∃a0 .Q.(φ ∧ EQ(a, φ))[a(τ1 , . . . , τar(a) ) := a0 (τi1 , . . . , τiar(a)−k )]
where ar(a0 ) = ar(a) − k and {i1 , . . . , iar(a)−k } = {1, . . . , ar(a)} \ {j1 , . . . , jk }.
4 The sets ΦL and ΦP
In this section we characterize the subset of formulae in Φ for which we can prove
that satisfiability is decidable by means of Theorems 1 and 2.
For a formula φ ∈ Φ, we say that the variable x is in the scope of function a
iff there is a term a(τi , . . . , τr(f ) ) ∈ App(a, φ) s.t. x appears in some τi .
We say that φ ∈ Φ is a basic formula iff it has the form Q.φ0 , where Q ∈ Q,
Bnd(φ0 ) = ∅ and no function symbol a with ar(a) > 1 is universally quantified by
Q. Hence, for some φ0 with Bnd(φ0 ) = ∅, E1 , . . . , En+1 in E (recall that ε ∈ E),
and real variables x1 , . . . , xn , a basic formula has the form
E1 .∀x1 . . . . En .∀xn .En+1 .φ0 .
For a basic formula ∃a.E1 .∀x1 . . . . En .∀xn .En+1 .φ, the following definition
gives a condition ensuring that, by iteratively applying Th. 1, all occurrences of
a(τ1 , . . . , τar(a) ) ∈ App(a, φ) can be substituted by terms a0 (τi1 , . . . , τim ) s.t. no
universally quantified variable xi is in the scope of a0 .
Definition 7. Given the basic-formula φ = ∃a.E1 .∀x1 . . . . En .∀xn .En+1 .φ0 , let
j be the maximal index in {1, . . . , n} s.t. xj is in the scope of a. Then we say
that a is a sequenced-function, denoted as S-function for short, iff for each index
i ∈ {1, . . . , j} there exists a set of indexes Sxi 6= ∅ s.t. a is Sxi -fixed on xi in φ.
Moreover, for each term a(τ1 , . . . , τar(a) ) ∈ App(a, φ0 ), for all argument terms
τh we have either:
– ID(τh ) ⊆ Free(φ),
– or xl ∈ ID(τh ) for some l ∈ {1, . . . , j}.
The idea behind Def. 7 is that φ = ∃a.E1 .∀x1 . . . . En .∀xn .En+1 .φ0 can be
mapped through j application of Th. 1 to an equivalent formula of the form
E1 .∀x1 . . . . Ej .∀xj ∃a0 .Ej+1 .∀xj+1 . . . En .∀xn .En+1 .φ00 , where all occurrences of
a(τ1 , . . . , τar(a) ) ∈ App(a, φ0 ) have been replaced by occurrences of a0 (τi1 , . . . , τim )
in φ00 s.t. no universally quantified xi is in the scope of a0 .
Example 7. The formula ∃b.∀x.∃a.∀y. x < y ⇒ a < b(y) does not respect Def.
7, since y is in the scope of b and b is not {1}-fixed on x. Since b is not {1}-fixed
on x, we cannot apply Th. 1 to b and x and the formula cannot be transformed
by applying Th. 1.
The formula ∃a.∃c.∀x.∀y. x < y ⇒ a(x) < c(y, x) respects Def. 7, since a is
{1}-fixed on x and c is {2}-fixed on x and {1}-fixed on y. By applying Th. 1 to
a and x we get the equivalent formula ∃c.∀x.∃a0 .∀y. x < y ⇒ a0 < c(y, x). Then,
by applying Th. 1 to c and x we get the equivalent formula ∀x.∃a0 .∃c0 .∀y. x <
y ⇒ a0 < c0 (y). Finally, by applying Th. 1 to c0 and y, we get the formula
∀x.∃a0 .∀y.∃c00 . x < y ⇒ a0 < c00 with only real variables.
Our aim is now to formally define a sequenced formula as a formula in
Φ in which all functions are sequenced functions. For the basic formula φ of
the form E1 .∀x1 . . . . En .∀xn .En+1 .φ0 , we denote with Ex(i, φ) the set of ex-
istentially quantified function symbols that occur in Ei . Formally, we define
Ex(i, φ) = {a1 , . . . , am } if Ei has the form ∃a1 .∃a2 . . . ∃am ; in particular we
define Ex(1, φ) = {ai | ai is existentially quantified in E1 } ∪ Free(φ).
Definition 8. The set of sequenced-formulae, S-formulae for short, is the least
set closed under disjunction and conjunction that contains the basic formula
E1 .∀x1 . . . . En .∀xn .En+1 .φ with a ∈ Ex(i, φ) for some i = 1, . . . , n + 1 iff a is an
S-function for the subformula ∃a.Ei .∀xi . . . En .∀xn .En+1 .φ.
With ΦL we denote the set of S-formulae that are linear. With ΦP we de-
note the set of S-formulae φ s.t. no occurrence of predicate int( ) appears. For
instance, all formulae in Ex. 2 but the first, are in ΦL . Moreover, the formula in
Ex. 3 and the first formula of Ex. 2 are in ΦP .
Proposition 3. For each S-formula φ, there exists a S-formula φ0 disjunction
of basic formulae that is equivalent to φ.
From now on we suppose that each formula is of the form as in Proposition
3. As a result of Def. 7 and Def. 8, if φ is an S-formula, then each value assumed
by a function symbol a, that as to be an S-function, can be related with itself
and a fixed finite set of values assumed by a, whichever is its arity. The following
theorem proves that satisfiability is decidable for formulae in ΦL and ΦP .
Theorem 3. The satisfiability problem is decidable for ΦL and ΦP .
We now aim to show that the sets ΦL and ΦP of S-formulae are the biggest
decidable classes. In other terms, all requirements of Def. 7, and so of Def. 8,
are necessary to ensure that satisfiability is decidable. The result of [7] can be
used to prove that, if we relax the definition of S-formulae, the satisfiability
problem for ΦL and ΦP is undecidable. In fact, [7] uses functions to calculate
the satisfiability of formula with polynomial terms and integer variables.
Firstly we focus on ΦL . For instance, we can consider the generic polynomial
term τ ·h, where τ is a linear term and h is an integer variable. Let φ(sol,τ,h) be the
linear formula int(sol)∧sol = a(τ +h)∧a(τ +1) = τ ∧∀ l ∈ [τ +1, τ +h] . a(l+1) =
a(l) + τ. Notice that this formula is not an S-formula, since function symbol a
is not Sl -fixed on l, ∀ l ∈ [τ + 1, τ + h].
The value τ · h is equal to the integer value assumed by the variable sol which
satisfies φ(sol,τ,h) . In fact, sol = a(τ +h) = a(τ +h−1)+τ = a(τ +h−2)+2·τ =
· · · = a(τ + 1) + (h − 1) · τ = τ + (h − 1) · τ = h · τ.
By applying this technique recursively, a value of a polynomial term τ can be
easily written as an integer value assumed by a variable which satisfies a linear
formula. For instance, τ · h1 · h2 can be written as sol1 · h2 , where sol1 satisfies
the formula φ(sol1 ,τ,h1 ) . Now sol1 is trivially a linear term, and hence, τ · h1 · h2 is
equal to the value of sol2 of the valuations which satisfy φ(sol1 ,τ,h1 ) ∧φ(sol2 ,sol1 ,h2 ) .
As a consequence, a polynomial formula τ ∼ 0 can be written as an equivalent
linear formula. Hence the satisfiability problem for ΦL is undecidable if we relax
the definition of S-functions and, consequently, of S-formulae, by removing the
S-fixed property.
We now take on the case of ΦP . The satisfiability of a formula with polynomial
terms and real variables is decidable. But we can use the functions to force a
real variable to be an integer. For instance, let τ ∼ 0 be a formula on integer
variables; we can write a formula φ, with no occurrences of predicate int( ), s.t.
τ ∼ 0 is satisfiable iff φ is.
Let {k1 , . . . , kn } be the integer variables which appear in τ , and {x1 , . . . , xn }
be a set of real variables. Let τ 0 = τ [k1 := x1 ] . . . [kn := xn ]. It is sufficient to
consider asVthe formula φ the following formula:
τ 0 ∼ 0 ∧ i∈[1,n] (xi ≥ 0 ⇒ a(xi ) = xi ) ∧ (xi < 0 ⇒ a(−xi ) = −xi ) ∧ ∀y.(0 ≤
y ∧ y < 1 ⇒ a(y) = 0) ∧ (y ≥ 1 ⇒ a(y) = a(y − 1) + 1).
We notice that, as in the previous case, function symbol a, which expresses
the integer part of a real variable, is not an S-function, since it is not Sy -fixed on
y in φ. Thus, φ 6∈ ΦP . We are going to show that, for each v |= φ, if xi is positive,
then a(xi ) = xi iff xi is a natural. If this holds, then the satisfiability problem
for φ is undecidable and therefore we cannot relax the definition of S-formula
without loosing decidability.
Let us suppose that v |= φ and a(xi ) = xi , then there exist ∈ [0, 1) and
k ∈ IN s.t. v(a(x)) = v(a()) + k. But, for each y < 1, it holds that a(y) = 0,
and therefore v(a()) = 0. Hence v(x) = v(a(x)) = v(a()) + k = k, for some
natural k. Conversely, if v is a valuation where v |= φ and v(x) is a natural, then
a(v(x)) = a(v(x)−1)+1. Since v(x) is a natural value, v(a(x)) = v(a(0))+v(x) =
0 + v(x) = v(x). Hence a(x) = x. Now it is obvious that if xi is negative, then
it is an integer iff a(−xi ) = −xi . So we can conclude as above that satisfiability
is not decidable for formulae not in ΦP .
Examples studied above, show that requirements of Def. 7, and so of Def. 8,
are necessary to ensure that satisfiability is decidable. Thus, the sets ΦL and ΦP
are the biggest decidable classes.
5 Modeling sets with ΦL and ΦP
The sets of formulae ΦL and ΦP are sufficient to model sets and strings.
In the following we show how to write classical operators and properties on
sets of integers and reals, where A and B are sets of n-tuples.
– A = {(x1 , . . . , xn ) | φ} where φ is a formula with only real variable, can be
expressed with the formula ∀x1 . . . . ∀xn .aA (x1 , . . . , xn ) = 1 ⇔ φ
– (τ1 , . . . , τn ) ∈ A can be expressed by the formula aA (τ1 , . . . , τn ) = 1
– A = B ∩ C can be expressed by the formula
∀x1 , . . . , xn . aA (x1 , . . . , xn ) = 1 ⇔ aB (x1 , . . . , xn ) = 1 ∧ aC (x1 , . . . , xn ) = 1
– A = B ∪ C can be expressed by the formula
∀x1 . . . . ∀xn .aA (x1 , . . . , xn ) = 1 ⇔ aB (x1 , . . . , xn ) = 1 ∨ bC (x1 , . . . , xn ) = 1
– A = B \ C can be expressed be the formula
∀x1 . . . . ∀xn .aA (x1 , . . . , xn ) = 1 ⇔ aB (x1 , . . . , xn ) = 1 ∧ aC (x1 , . . . , xn ) 6= 1
– A ⊆ B can be expressed by the formula
∀x1 . . . ∀xn .aA (x1 , . . . , xn ) = 1 ⇒ aB (x1 , . . . , xn ) = 1
– |A| = 0 can be expressed by the formula
∀x1 . . . ∀xn .aA (x1 , . . . , xn ) 6= 1
– |A| ≤ k can be expressed by the formula
∃y11 .∃y21 . . . ∃ynk .∀x1 . . . ∀xn .aA (x1 , . . . , xn ) = 1 ⇒ i∈[1,k] j∈[1,n] xj = yji
W V
– |A| ≥ k can be expressed by the formula
j
∃x11 .∃x12 . . . ∃xkn . i∈[1,k] aA (xi1 , . . . , xin ) = 1 ∧ j6=i i
V V V
h∈[1,n] xh 6= xh .
We note that the formulae above are closed on conjunction and disjunction.
Example 8. The formula ∃B.∃C∃z.A = {x | ∃w.w2 x3 +2x+1 ≤ z}∧B = A\C ∧
|B| 6= 0 is satisfiable iff ∃aB .∃.aC ∃.z.∃y.∀x.∃w.(aA (x) = 1 ⇔ w2 x3 + 2x + 1 ≤
z) ∧ (aB (x) = 1 ⇔ aA (x) = 1 ∧ aC (x) 6= 1) ∧ aB (y) = 1 This last formula is in
ΦP , and therefore the satisfiability is decidable.
In the example above we have considered sets of reals where formulae to
express properties are polynomial. If one wants to consider also integers one
must restrict to linear formulae.
Example 9. The formula ∃B.∃C.∃z.A = {(x, y) | int(x + y) ∧ z = 2x} ∧ B =
A\C ∧B 6= ∅ is satisfiable iff ∃aB .∃aC .∃z.∀x.∀y.∃w1 .∃w2 .aA (x, y) = 1 ⇔ int(x+
y) ∧ z = 2x) ∧ ((aB (x, y) = 1 ⇔ aA (x, y) = 1 ∧ aC (x, y) 6= 1) ∧ aB (w1 , w2 ) = 1
This last formula is in ΦL , and therefore the satisfiability is decidable.
6 Conclusions and Related works
We have proved that, in the framework of Arithmetical Logics, quantifier elim-
ination for formulae with functions cannot exist, and hence we have defined a
technique for decreasing the arity of functions appearing in a given formulae.
We have proved the correctness of the method and we have used it to prove
the decidability of the satisfiability problem for two classes of formulae. These
classes have sufficient power to model theories as those of sets and strings.
In the literature several classes and methods have been studied. In [4] the
decidable classes are surveyed. First of all, the paper considers classes that are
subclasses of first order logics (hence no predicates and functions can be quanti-
fied). In [26] formulae with prefixes in ∃∗ ∀∗ and without functions are considered.
Formulae with prefixes in ∃∗ ∀2 ∃∗ and without functions and equality predicates
are tackled in [11], [24] and [27]. Formulae without equality predicate, and with
unary predicate and functions are studied in [19] and [12]. In [22] and [13] pre-
fixes in ∃∗ ∀∃∗ for formulae without equality predicates are considered, and in [14]
existential quantified formulae are tackled. Finally universal quantified formulae
with unary predicates and at most one unary function are studied in [3]. For
all these classes, the finite model property is decidable, i.e. it is decidable to
check whether there exists a model with a given finite complexity satisfying a
given formula. The classes we define have a decidable result for generic model,
moreover also quantifications on functions are considered. We do not consider
predicates but these can be simulated by a function that can assume values in
the set {0, 1}, where 0 represents f alse, and 1 represents true.
Monadic second order formulae are studied in [25] (see [15] and [33] for sur-
veys). More precisely, a second order logic is defined (with unary predicates and
at most one unary function) for which the satisfiability problem is decidable.
There are several differences between this logic and those we consider. First of
all, we have general arity but restrictions on the quantifications of variables and
functions. Moreover, we consider reals and integers. In [25] only the natural field
is considered (in [28] it is proved that the satisfiability problem for monadic sec-
ond order logic on real field is undecidable). Finally we consider polynomial and
general linear formulae, instead of formulae of the form x < y as done in [25].
The class defined in [29] contains the set of second order formulae with prefixes in
∃∗ ∀∃∗ , with predicates and one function. The classes we consider have a similar
prefix, but the other differences shown for the class in [25] still hold.
Hence we must compare our classes with the classes allowing real and integer
variables. Decidability results in this framework in usually given by a quanti-
fier elimination technique. In [9] quantifier elimination for formulae which are
linear and which contain real variables is studied. In [32] Tarski considers the
general case of polynomial formulae on real variables. In the case of integer vari-
ables, if one considers linear formulae without quantifier on integer variables,
then the satisfiability is decidable (see [36] and [18]). If one deals with First Or-
der Logic on Linear Formulae with Integer Variables (called Presburger Arith-
metic), [8] offers a quantifier elimination algorithm which is given by introducing
equivalences modulo a natural value. In [10] it is shown that it is decidable in
double-exponential time. These first studies were directed to prove decidability.
In recent years such quantifier elimination procedure has turned out to allow
important applications e.g. in simulation and optimization, control theory and
applied computational geometry ( [1], [5], [6], [17] and [35]). Hence improvements
to the efficiency of the algorithms are done in [20] and [31]. When one tackles
formulae with mixed integer and real variables, techniques of quantifier elimina-
tion given for real field still hold. Conversely, these techniques do not hold for
the case of integer variables. In [34], a quantifier algorithm for mixed variables
is proposed. In this case, together with equivalences modulo a natural value, a
function which gives the integer part of a real value is considered. All the classes
mentioned consider first order logics without functions symbols. Hence they are
subclasses of ΦL and ΦP . For formulae with exponential functions, which our
logics cannot express, quantifier elimination exists for some cases (see [21]).
The satisfiability problem for High Order Arithmetical Logics (where func-
tion are quantifiable) is undecidable (due to the already mentioned undecidabil-
ity result holding for polynomial formulae on integer variables). This bad result
holds also if one considers linear formulae (see [7] and [16]). If uninterpreted
functions are considered with linear formulae then the decidability holds [30].
It is immediate to see that the classes defined in this paper extend the class of
uninterpreted functions by simply considering formulae of the form ∃a.∀x.φ.
References
1. Abdallah, C. T., Dorato, P., Yang, W., Liska, R., and Steinberg, S.: Applications
of Quantifier Elimination Theory to Control System Design. In Proc. of the 4th
IEEE Mediterranean Symposium on Control and Automation (1996), IEEE, 340
– 345.
2. Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland, Amster-
dam, 1954.
3. Ash, C.: Sentences with Finite Models. Weitschr. f. math. Logik u. Grundlagen d.
Math. 21 (1975), 401– 404.
4. Börger, E., Grädel, E., and Gurevich, Y.: The Classical Decision Problem. Springer,
1997.
5. Dolzmann, A., and Sturm, T.: Redlog: Computer Algebra Meets Computer Logic.
ACM SIGSAM Bulletin 31 (1997), 2–9.
6. Dolzmann, A., Sturm, T. and Weispfenning, V.: A New Approach for Automatic
Theorem Proving in Real Geometry. Journal of Automated Reasoning 21 (1998),
357-380.
7. Downey, P.: Undecidability of Presburger Arithmetic with a Single Monadic Predi-
cate Letter. Technical Report 18-72, Center for Research in Computing Technology,
Harvard Univ., 1972.
8. Enderton, H. B. .: Mathematical Introduction to Logic. Academic Press, 1972.
9. Ferrante, J., and Rackoff, C.: A Decision Procedure for First-order Theory of Real
Addition with Order. SIAM Journal on Computing 4 (1975), 69–76.
10. Fischer, M. J., and Rabin, M. O.: Super-Exponential Complexity of Presburger
Arithmetic. Complexity of Computation, SIAM-AMS Proc. 7 (1974), 27–42.
11. Godel, K.: Ein Spezialfall des Entscheidungsproblems der theoretischen Logik.
Ergebn. math. Kolloq. 2 (1932), 27–28.
12. Gurevich, Y.: The Decision Problem for the Logic of Predicates and Operations.
Algebra and Logic 8 (1969), 160–174.
13. Gurevich, Y.: Formulas with one ∀. Selected Questions in Algebra and Logics.
Nauka, Novosibirsk, 1973, 97–110.
14. Gurevich, Y.:The Decision Problem for Standard Classes. Journal of Symbolic
Computation 41 (1976), 460–464.
15. Gurevich, Y.:Monadic Second-order Theories. Model-theoretic Logics, Springer,
Berlin, 1985, 479–506.
16. Halpern J. Y.: Presburger Arithmetic with Unary Predicates is Π11 Complete.
Journal of Symbolic Logic 56, 1991, 637–642.
17. Honga, H., and Liskab, R. (Eds.): Special Issue on Applications of Quantifier
Elimination. Journal of Symbolic Computation 24 (1997).
18. Lenstra H.W.: Integer Programming with a Fixed Number of Variables. Mathemat-
ics of Operations Research 8 (1983), 538–548.
19. Löb M.: Decidability of The Monadic Predicate Calculus with Unary Function
Symbols. Journal of Symbolic Logic 32 (1967), pp. 563.
20. Loos, R., and Weipfenning, V.:Applying Linear Quantifier Elimination. The Com-
puter Journal 36 (1993), 450–462.
21. Marker, D.: Model Theory and Exponentiation. Notices AMS 43 (1996), 753–759.
22. Maslov, S., and Orevkov, V.: Decidable Classes Reducing to One-quantifier Class.
Proc. Steklov Ins. Steklov Math 121 (1972), 61–72.
23. Matijasevic, J. Y.: Hilbert’s Tenth Problem. MIT press, Cambridge, 1993.
24. Kalmar, L.: Uber die Erfullbarkeit derjenigen Zahlausdrucke, welehe in der Nor-
malform zwei benachbarte Allzeichen enthalten. Math. Ann. 108 (1933), 466-484.
25. Rabin, M.: Decidability of Second Order Theories and Automata on Infinite trees.
Trans. Amer. Math. Soc. 141 (1969), 1–35.
26. Ramsey, F. P.: On a Problem in Formal Logic. Proc. of the London Mathematical
Society 30 (1930), 264–286.
27. Schutte, K.: Untersuchungen zum entscheidungsproblem der mathematischen logik.
Math. Annal. 109 (1934), 572–603.
28. Shelah, S.: The Monadic Theory of Order. Ann. of Math. 102 (1975), 379–419.
29. Shelah, S.: Decidability of a Portion of the Predicate Calculus. Israel Journal of
Mathematics, 28 (1977), 32–44.
30. Shostak, R.E. : A Practical Decision Procedure for Arithmetic with Functions Sym-
bols. Journal of ACM 26 (1979), 351–360.
31. Subrami, K.: An Analysis of Quantified Linear Programs. Proc. 4th Int. Conference
on Discrete Mathematics and Theoretical Computer Science, Lecture and notes in
Computer Science, 2731 (2003), Springer, 265–277.
32. Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University
of California Press, Second Edition, 1951.
33. Thomas, W.: Languages, Automata, and Logic. Handbook of Formal Languages, 3
(1997), Springer Verlag, 389–455.
34. Weispfenning, V.: Mixed Real-Integer Linear Quantifier Elimination. Proceedings
of the ACM International Symposium on Symbolic and Algebraic Computation,
1999.
35. Weispfenning, V.: A New Approach to Quantifier Elimination for Real Algebra.
In Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and
Monographs in Symbolic Computation, Springer, 1998, 376–392.
36. Williams, H. P.: Fourier-Motzkin Elimination Extension to Integer Programming.
Journal of Combinatorial Theory 21 (1976), 118–123.