Rewrite systems for natural, integral, and rational arithmetic


We give algebraic presentations of the sets of natural numbers, integers, and rational numbers by convergent rewrite systems which moreover allow efficient computations of arithmetical expressions. We then use such systems in the general normalized completion algorithm, in order to compute Gröbner bases of polynomial ideals over Q.

full paper