Proceedings of CADE 21, the 21st International Conference on Automated Deduction. Springer LNCS vol. 4603, pp. 51-66, 2007.
@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"}