A Function Elimination Method for Checking Satis ability of Arithmetical Logics

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 satis ability problem for two classes of formulae allowing linear and polynomial terms.

Introduction

A branch of First Order Logics are Arithmetical Logics. Arithmetical Logics consider quanti ed formulae where variables are either reals or integers, and where functions in f+; g and relations in f<; =; >; ; g are used.

The satis ability problem deals with the existence of a valuation for variables, 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 ]). Di erent classes are considered to avoid such di culty, and several techniques can be used to prove decidability (see [ 4 ]). One of these techniques is based on the quanti er elimination approach. Given a formula with a quanti ed variable, the quanti er elimination deals with the problem of nding an equivalent formula without quanti ers.

The results of this paper are the following ones: we prove that quanti er 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 satis ability problem for two subclasses of formulae in the set of formulae with pre xes in (9 8) . The two classes (the rst one allowing real polynomial terms and the second one mixed linear terms) are su cient 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 de ned 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.

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 2 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. De nition 1. The set T of polynomial terms with rational coe cients, ranged over by , is de ned inductively by: ::= q j q a( 1; : : : ; ar(a)) j 1 + 2 j 1 2 where q 2 Q and a 2 F . The terms in T generated without using the multiplication 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 2 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 49 x (b(x + a(y2)))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) = fx; y; a; bg.

For a term 2 T and a valuation v 2 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 De nition 2. The set by:

of quanti ed formulae over T is de ned inductively ::=

0 j int( ) j 9a : 0 j : 1 j 1 _ 2 where ; 0 2 T , 2 f<; ; =; ; >g and a 2 F . Conjunction, implication and universal quanti cation 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 quanti ed formula 2 and a valuation v 2 V, we write v j= satis es . The relation j= is de ned as follows: if v v j= v j= 0 iff [ ]v [ 0]v v j= int( ) iff [ ]v 2 ZZ v j= 9a: 0 iff there exists a f : IRar(a) ! IR s.t. v[f =a] j= 0 v j= : 1 iff v 6j= 1 (namely v j= does not hold)

1 _ 2 iff v j= 1 or v j= 2:

For a formula 2 , we denote with J K the set of valuations in V that satisfy , formally J K = fv 2 V j v j= g. Two formulae 1 and 2 are equivalent iff J 1K = J 2K. 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-quanti ed in , and with Bnd( ) we denote the set of real variables and functions symbols quanti ed 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( ): 8x:a(x) a(x) = b(x; 1). { The function a assumes only integer values: 8x:int(a(x)). { The function a reaches x: 9y:a(y) = x. { The minimum of a is in position x: 8y:a(y) a(x). { The function a is binary: 8x:a(x) = 0 _ a(x) = 1. { The function a is monotone: 8x; y:x y ) a(x) a(y).

Given two terms 1; 2 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 . De nition 3. E = f9a: j a 2 F g is called the set of existential quanti cation pre xes, F = f8a: j a 2 F g is called the set of universal quanti cation pre xes, and Q = f9a:; 8a: j a 2 F g is called the set of quanti cation pre xes.

For instance, 9a:9b: is in E and 9a:8b: is in Q. From now on, without loss of generality we consider formulae of the form Q: where Q 2 Q, and Bnd( ) = ;.

2 De nition 4. A quanti ed formula 2 is satis able iff J K 6= ;. The satisability problem for consists in answering if is satis able.

The satis ability problem is in general undecidable if one considers quanti ed polynomial formulae on integer variables (see [ 23 ]). Di erent classes of formulae have been considered to avoid such a di culty. For quanti ed linear formulae on real and integer variables (without function symbols a with ar(a) > 0), the satis ability problem is decidable (see [ 34 ]). In fact, in this case quanti ers can be eliminated through quanti er elimination, which consists in transforming a formula 9x: where Bnd( ) = ; into an equivalent formula 0 s.t. Bnd( 0) = ;. For instance, 9x:5 < x^x < y can be transformed into the equivalent formula 5 < y. In general, quanti er 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 quanti er elimination cannot work, in general, for the formulae in . Proposition 1. Let be the formula 8x : 0 x < y ) a(x) = 0. There is no formula 0 2 with Bnd( 0) = ; equivalent to .

For a formula 9a: with Bnd( ) = ;, we say that a is an uninterpretated function. The satis ability of such a formula is decidable. In fact, by following [ 30 ], one can get a formula 0 equivalent to 9a: 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 satis ability is decidable according to [ 34 ]. For instance, 9a:a(4) a(k) can be turned into 9x:9y:x y ^ ((4 = k) ) (x = y)). The challenge is to extend this method to formulae not in the form 9a: with Bnd( ) = ;. This is immediate for formulae of the form 9a:9x: with Bnd( ) = ;, since such a formula is equivalent to 9x:9a: , which can be transformed to 9x: 0, to which quanti er elimination applies. The di culty is in the formulae of the form 9a:8x: and 8a:9x: . In next section we consider the case 9a:8x: since 8a:9x: = :9a:8x:: . 3

The function elimination method

In this section we give two results showing under which circumstances a function in a quanti ed 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 satis ability 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).

De nition 5. A term 2 T is determined by a real variable x iff [ ]v 6= [ ]v0 for all valuations v; v0 2 V s.t. v(x) 6= v0(x), and v(y) = v0(y) for all y 6= x.

For instance, the terms x3 +a(z) z2 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.

De nition 6. Let a 2 F , S f1; : : : ; ar(a)g with S 6= ;, x be a real variable and 2 . We say that a is S- xed on x in iff: { for each i 62 S and a( 1; : : : ; ar(a)) 2 App(a; ), it holds that x 62 ID( i); { for each i 2 S, there exists a term ^i determined by x s.t. ID(^i) Free( ) [ fxg and, for all a( 1; : : : ; ar(a)) 2 App(a; ), it holds that i = ^i.

Informally, a is S- xed 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 2 S and, for each i 2 S, the respective term i is unique and determined by x. This implies that, for each c; c0 2 IR with c 6= c0, the values of the argument terms i with i 2 S to which a is applied in [x := c] are di erent 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 quanti ed function symbol a. Example 3. We consider the following running example. Let r be the formula 9b:8x:8y:9a:8z:a(z + b(y3; x + 5)) = b(y3; b(y3; 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 f1g- xed on y in r. Then, b is not S- xed on x in r, for any S. Finally, a is not f g

1 - xed on any variable in r.

If a is S- xed on x in with f1; : : : ; ar(a)g n S = fi1; : : : ; img, and a0 is a function symbol s.t. ar(a0) = m, then let Sub(a; a0; S; ) denote the formula ( )f[a( 1; : : : ; ar(a)) := a0( i1 ; : : : ; im )] j a( 1; : : : ; ar(a)) 2 App(a; )g 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 2 , a function symbol a 2 F , a real variable x and a set S f1; : : : ; ar(a)g. If a is S- xed on x in , then

is equivalent to 8x:9a0: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: 8y:9b0:8x:9a:8z: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 functions with functions with less arguments.

Let 2 and a 2 F . With EQ(a; ) we denote the formula ^

^ a( 10 ;:::; a0r(a)) 2 App(a; ) i2[1;ar(a)] a( 1;:::; ar(a))

i = i0 ) a( 1; : : : ; ar(a)) = a( 10 ; : : : ; a0 r(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 9f:8y:P (y; f (y)), with P a predicate, is equivalent to 8y:9x:P (y; x). We apply the same strategy to formulae in . Theorem 2. Let 0 2 be the formula 9a: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

9a:9a0: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) 2 App(b0; 0r) we obtain the equivalent formula 8y:9b0:9w:8x:9a:8z: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 8y:9b0:9w:9t:8x:9a:8z: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 f g 1 - xed on x, thus obtaining the equivalent formula 8y:9w:9t:8x:9s:9a:8z: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 8y:9w:9t:8x:9s:9a:9a0:8z: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 f1g- xed on z, we obtain the equivalent formula 8y:9w:9t:8x:9s:9a0:8z:9a00: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 satis ability 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 2 be the formula 9a: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 9a:9a0:Q:( ^ EQ(a; ))[a( 1; : : : ; ar(a)) := a0( i1 ; : : : ; iar(a) k )] where ar(a0) = ar(a)

k and fi1; : : : ; iar(a) kg = f1; : : : ; ar(a)g n fj1; : : : ; jkg. 4

The sets

L and

P In this section we characterize the subset of formulae in for which we can prove that satis ability is decidable by means of Theorems 1 and 2.

For a formula 2 , we say that the variable x is in the scope of function a iff there is a term a( i; : : : ; r(f)) 2 App(a; ) s.t. x appears in some i.

We say that 2 is a basic formula iff it has the form Q: 0, where Q 2 Q, Bnd( 0) = ; and no function symbol a with ar(a) > 1 is universally quanti ed by Q. Hence, for some 0 with Bnd( 0) = ;, E1; : : : ; En+1 in E (recall that " 2 E ), and real variables x1; : : : ; xn, a basic formula has the form

E1:8x1: : : : En:8xn:En+1: 0:

For a basic formula 9a:E1:8x1: : : : En:8xn:En+1: , the following de nition gives a condition ensuring that, by iteratively applying Th. 1, all occurrences of a( 1; : : : ; ar(a)) 2 App(a; ) can be substituted by terms a0( i1 ; : : : ; im ) s.t. no universally quanti ed variable xi is in the scope of a0.

De nition 7. Given the basic-formula = 9a:E1:8x1: : : : En:8xn:En+1: 0, let j be the maximal index in f1; : : : ; ng 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 2 f1; : : : ; jg there exists a set of indexes Sxi 6= ; s.t. a is Sxi - xed on xi in . Moreover, for each term a( 1; : : : ; ar(a)) 2 App(a; 0), for all argument terms h we have either: { ID( h) Free( ), { or xl 2 ID( h) for some l 2 f1; : : : ; jg.

The idea behind Def. 7 is that = 9a:E1:8x1: : : : En:8xn:En+1: 0 can be mapped through j application of Th. 1 to an equivalent formula of the form E1:8x1: : : : Ej :8xj 9a0:Ej+1:8xj+1 : : : En:8xn:En+1: 00, where all occurrences of a( 1; : : : ; ar(a)) 2 App(a; 0) have been replaced by occurrences of a0( i1 ; : : : ; im ) in 00 s.t. no universally quanti ed xi is in the scope of a0.

Example 7. The formula 9b:8x:9a:8y: x < y ) a < b(y) does not respect Def. 7, since y is in the scope of b and b is not f1g- xed on x. Since b is not f g 1 - xed on x, we cannot apply Th. 1 to b and x and the formula cannot be transformed by applying Th. 1.

The formula 9a:9c:8x:8y: x < y ) a(x) < c(y; x) respects Def. 7, since a is f1g- xed on x and c is f2g- xed on x and f1g- xed on y. By applying Th. 1 to a and x we get the equivalent formula 9c:8x:9a0:8y: x < y ) a0 < c(y; x). Then, by applying Th. 1 to c and x we get the equivalent formula 8x:9a0:9c0:8y: x < y ) a0 < c0(y). Finally, by applying Th. 1 to c0 and y, we get the formula 8x:9a0:8y:9c00: x < y ) a0 < c00 with only real variables.

Our aim is now to formally de ne a sequenced formula as a formula in in which all functions are sequenced functions. For the basic formula of the form E1:8x1: : : : En:8xn:En+1: 0, we denote with Ex(i; ) the set of existentially quanti ed function symbols that occur in Ei. Formally, we de ne Ex(i; ) = fa1; : : : ; amg if Ei has the form 9a1:9a2 : : : 9am; in particular we de ne Ex(1; ) = fai j ai is existentially quanti ed in E1g [ Free( ). De nition 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:8x1: : : : En:8xn:En+1: with a 2 Ex(i; ) for some i = 1; : : : ; n + 1 iff a is an S-function for the subformula 9a:Ei:8xi : : : En:8xn:En+1: .

With L we denote the set of S-formulae that are linear. With P we denote the set of S-formulae s.t. no occurrence of predicate int( ) appears. For instance, all formulae in Ex. 2 but the rst, are in L. Moreover, the formula in Ex. 3 and the rst 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 xed nite set of values assumed by a, whichever is its arity. The following theorem proves that satis ability is decidable for formulae in L and P .

Theorem 3. The satis ability 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 satis ability is decidable. The result of [ 7 ] can be used to prove that, if we relax the de nition of S-formulae, the satis ability problem for L and P is undecidable. In fact, [ 7 ] uses functions to calculate the satis ability 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) = ^8 l 2 [ +1; +h] : a(l+1) = a(l) + : Notice that this formula is not an S-formula, since function symbol a is not Sl- xed on l; 8 l 2 [ + 1; + h].

The value h is equal to the integer value assumed by the variable sol which satis es (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 satis es a linear formula. For instance, h1 h2 can be written as sol1 h2, where sol1 satis es 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 satis ability problem for L is undecidable if we relax the de nition of S-functions and, consequently, of S-formulae, by removing the S- xed property.

We now take on the case of P . The satis ability 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 satis able iff is.

Let fk1; : : : ; kng be the integer variables which appear in , and fx1; : : : ; xng be a set of real variables. Let 0 = [k1 := x1] : : : [kn := xn]. It is su cient to consider as the formula the following formula:

0 0 ^ Vi2[1;n] (xi 0 ) a(xi) = xi) ^ (xi < 0 ) a( xi) = xi) ^ 8y:(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- xed on y in . Thus, 62 P . We are going to show that, for each v j= , if xi is positive, then a(xi) = xi iff xi is a natural. If this holds, then the satis ability problem for is undecidable and therefore we cannot relax the de nition of S-formula without loosing decidability.

Let us suppose that v j= and a(xi) = xi, then there exist 2 [0; 1) and k 2 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 j= 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 satis ability 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 satis ability 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 su cient 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 = f(x1; : : : ; xn) j g where is a formula with only real variable, can be expressed with the formula 8x1: : : : 8xn:aA(x1; : : : ; xn) = 1 , { ( 1; : : : ; n) 2 A can be expressed by the formula aA( 1; : : : ; n) = 1 { A = B \ C can be expressed by the formula

8x1; : : : ; xn: aA(x1; : : : ; xn) = 1 , aB(x1; : : : ; xn) = 1 ^ aC (x1; : : : ; xn) = 1 { A = B [ C can be expressed by the formula

8x1: : : : 8xn:aA(x1; : : : ; xn) = 1 , aB(x1; : : : ; xn) = 1 _ bC (x1; : : : ; xn) = 1 { A = B n C can be expressed be the formula

8x1: : : : 8xn:aA(x1; : : : ; xn) = 1 , aB(x1; : : : ; xn) = 1 ^ aC (x1; : : : ; xn) 6= 1 { A B can be expressed by the formula

8x1 : : : 8xn:aA(x1; : : : ; xn) = 1 ) aB(x1; : : : ; xn) = 1 { jAj = 0 can be expressed by the formula

8x1 : : : 8xn:aA(x1; : : : ; xn) 6= 1 { jAj k can be expressed by the formula

9y11:9y21 : : : 9ynk:8x1 : : : 8xn:aA(x1; : : : ; xn) = 1 ) Wi2[1;k] Vj2[1;n] xj = yji { jAj k can be expressed by the formula 9x11:9x21 : : : 9xkn: Vi2[1;k] aA(xi1; : : : ; xin) = 1 ^ Vj6=i Vh2[1;n] xih 6= xjh: We note that the formulae above are closed on conjunction and disjunction. Example 8. The formula 9B:9C9z:A = fx j 9w:w2x3 + 2x + 1 zg ^ B = A n C ^ jBj 6= 0 is satis able iff 9aB:9:aC 9:z:9y:8x:9w:(aA(x) = 1 , w2x3 + 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 satis ability 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 9B:9C:9z:A = f(x; y) j int(x + y) ^ z = 2xg ^ B = AnC ^B 6= ; is satis able iff 9aB:9aC :9z:8x:8y:9w1:9w2: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 satis ability is decidable.

Conclusions and Related works

We have proved that, in the framework of Arithmetical Logics, quanti er elimination for formulae with functions cannot exist, and hence we have de ned 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 satis ability problem for two classes of formulae. These classes have su cient 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 rst order logics (hence no predicates and functions can be quantied). In [ 26 ] formulae with pre xes in 9 8 and without functions are considered. Formulae with pre xes in 9 829 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 ] prexes in 9 89 for formulae without equality predicates are considered, and in [ 14 ] existential quanti ed formulae are tackled. Finally universal quanti ed formulae with unary predicates and at most one unary function are studied in [ 3 ]. For all these classes, the nite model property is decidable, i.e. it is decidable to check whether there exists a model with a given nite complexity satisfying a given formula. The classes we de ne have a decidable result for generic model, moreover also quanti cations on functions are considered. We do not consider predicates but these can be simulated by a function that can assume values in the set f0; 1g, where 0 represents f alse, and 1 represents true.

Monadic second order formulae are studied in [ 25 ] (see [ 15 ] and [ 33 ] for surveys). More precisely, a second order logic is de ned (with unary predicates and at most one unary function) for which the satis ability problem is decidable. There are several di erences between this logic and those we consider. First of all, we have general arity but restrictions on the quanti cations of variables and functions. Moreover, we consider reals and integers. In [ 25 ] only the natural eld is considered (in [ 28 ] it is proved that the satis ability problem for monadic second order logic on real eld is undecidable). Finally we consider polynomial and general linear formulae, instead of formulae of the form x < y as done in [ 25 ]. The class de ned in [ 29 ] contains the set of second order formulae with pre xes in 9 89 , with predicates and one function. The classes we consider have a similar pre x, but the other di erences 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 quantier elimination technique. In [ 9 ] quanti er 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 variables, if one considers linear formulae without quanti er on integer variables, then the satis ability is decidable (see [ 36 ] and [ 18 ]). If one deals with First Order Logic on Linear Formulae with Integer Variables (called Presburger Arithmetic), [ 8 ] o ers a quanti er 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 rst studies were directed to prove decidability. In recent years such quanti er 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 e ciency of the algorithms are done in [ 20 ] and [ 31 ]. When one tackles formulae with mixed integer and real variables, techniques of quanti er elimination given for real eld still hold. Conversely, these techniques do not hold for the case of integer variables. In [ 34 ], a quanti er 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 rst order logics without functions symbols. Hence they are subclasses of L and P . For formulae with exponential functions, which our logics cannot express, quanti er elimination exists for some cases (see [ 21 ]).

The satis ability problem for High Order Arithmetical Logics (where function are quanti able) is undecidable (due to the already mentioned undecidability 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 de ned in this paper extend the class of uninterpreted functions by simply considering formulae of the form 9a:8x: .

References

1. Abdallah , C. T. , Dorato , P. , Yang , W. , Liska , R. , and Steinberg , S. : Applications of Quanti er 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, Amsterdam, 1954 .

3. Ash , C. : Sentences with Finite Models . Weitschr. f. math. Logik u. Grundlagen d. Math. 21 ( 1975 ), 401 { 404 .

4. Borger, E., Gradel, 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 Predicate 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 Racko , 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 8. 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 Quanti er Elimination . Journal of Symbolic Computation 24 ( 1997 ).

18. Lenstra H.W. : Integer Programming with a Fixed Number of Variables . Mathematics of Operations Research 8 ( 1983 ), 538 { 548 .

19. L ob 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 Quanti er Elimination . The Computer 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-quanti er 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 Normalform zwei benachbarte Allzeichen enthalten . Math. Ann. 108 ( 1933 ), 466 - 484 .

25. Rabin , M. : Decidability of Second Order Theories and Automata on In nite 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 Symbols . Journal of ACM 26 ( 1979 ), 351 { 360 .

31. Subrami , K. : An Analysis of Quanti ed 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 Quanti er Elimination . Proceedings of the ACM International Symposium on Symbolic and Algebraic Computation , 1999 .

35. Weispfenning , V.: A New Approach to Quanti er Elimination for Real Algebra . In Quanti er 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 .