We present a uniform algorithm for proving automatically a fairly wide class of elementary facts connected with integer divisibility. The assertions that can be handled are those with a limited quantifier structure involving addition, multiplication and certain number-theoretic predicates such as 'divisible by', 'congruent' and 'coprime'; one notable example in this class is the Chinese Remainder Theorem (for a specific number of moduli). The method is based on a reduction to ideal membership assertions that are then solved using Gröbner bases. As well as illustrating the usefulness of the procedure on examples, and considering some extensions, we prove a limited form of completeness for properties that hold in all rings. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Harrison, J. (2007). Automating elementary number-theoretic proofs using Gröbner bases. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4603 LNAI, pp. 51–66). Springer Verlag. https://doi.org/10.1007/978-3-540-73595-3_5
Mendeley helps you to discover research relevant for your work.