Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleAutomating Elementary Number-Theoretic Proofs Using Gröbner Bases
Author(s) John Harrison
TypeArticle in Journal
AbstractWe 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.
JournalAutomated Deduction – CADE-21
SeriesLecture Notes in Computer Science
PublisherSpringer Verlag
Translation No
Refereed Yes