Quantifier elimination for elementary geometry and elementary affine geometry

RAFAEL GRIMSON; BART KUIJPERS; WALIED OTHMAN

MATHEMATICAL LOGIC QUARTERLY

WILEY-V C H VERLAG GMBH

Lugar: Weinheim; Año: 2012 vol. 58 p. 399 - 416

0942-5616

We introduce new first-order languages for the elementary n-dimensional geometry and elementary n-dimensional affine geometry (n >= 2), based on extending Tarski's classical languages (containing only the betweenness relation and both the betweenness and the congruence relations, respectively), with new function symbols. We show that the associated theories admit effective quantifier elimination.