Rewrite systems for natural, integral, and rational arithmetic

Abstract: 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 normalised completion algorithm, in order to compute Gröbner bases of polynomial ideals over ℚ.

This document was translated from L^AT_EX by H^EV^EA.