Marius Bozga and Radu Iosif
On Decidability within the Arithmetic of Addition and Divisibility (2004)
On Decidability within the Arithmetic of Addition and Divisibility (2004)
TR-2004-18.ps
Keywords: arithmetic theories, decidability, quantifier elimination, quantitative analysis
Abstract: The arithmetic of natural numbers with addition and divisibility has been shown undecidable as a consequence of the fact that multiplication of natural numbers can be interpreted into this theory, as shown by J. Robinson cite{robinson49}. The most important decidable subsets of the arithmetic of addition and divisibility are the arithmetic of addition, proved by M. Presburger cite{presburger29}, and the purely existential subset, proved by L. Lipshitz cite{lipshitz}. In this paper we define a new decidable fragment of the form $Q z Q_1 x_1 ldots Q_n x_n varphi(vec{x}, z)$ where the only variable allowed to occur to the left of the divisibility sign is $z$. For this form, called lonediv in the paper, we show the existence of a quantifier elimination procedure which always leads to formulas of Presburger arithmetic. Subsequently we generalize the lonediv form to $exists z_1, ldots exists z_m Q_1 x_1 ldots Q_n x_n varphi(vec{x}, vec{z})$, where the only variables appearing on the left of divisibility are $z_1, ldots, z_n$. For this form, called elmanydiv, we show decidability of the positive fragment, namely by reduction to the existential theory of the arithmetic with addition and divisibility. The lonediv, elmanydiv fragments were inspired by a real application in the field of program verification. We considered the satisfiability problem for a program logic used for quantitative reasoning about memory shapes, in the case where each record has at most one pointer field. The reduction of this problem to the positive subset of elmanydiv is sketched in the end of the paper.
