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\"obner bases.
Author(s) John Harrison
TypeBook, Chapter in Book, Conference Proceeding
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.
URL http://link.springer.com/chapter/10.1007%2F978-3-540-73595-3_5
PublisherBerlin: Springer
Translation No
Refereed No