We introduce new first-order languages for the elementary n-dimensional geometry and elementary n-dimensional affine geometry , based on extending equation image and equation image, respectively, with new function symbols. Here, β stands for the betweenness relation and ≡ for the congruence relation. We show that the associated theories admit effective quantifier elimination.

We identify the locally finite graphs that are quantifier-eliminable and their first order theories in the signature of distance predicates. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

We develop a notion of cell decomposition suitable for studying weak p-adic structures definable). As an example, we consider a structure with restricted addition.