Automating elementary number-theoretic proofs using Gröbner bases

John Harrison.

Proceedings of CADE 21, the 21st International Conference on Automated Deduction. Springer LNCS vol. 4603, pp. 51-66, 2007.

Abstract:

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.

DVI, PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-divisibility,
        author          = "John Harrison",
        title           = "Automating elementary number-theoretic proofs using
                           Gr{\"o}bner bases",
        editor          = "Frank Pfenning",
        booktitle       = "Proceedings of the 21st International Conference on
                           Automated Deduction, CADE 21",
        address         = "Bremen, Germany",
        year            = 2007,
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 4603,
        pages           = "51--66"}