{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T04:48:01Z","timestamp":1755838081923},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_5","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T05:31:33Z","timestamp":1188451893000},"page":"51-66","source":"Crossref","is-referenced-by-count":12,"title":["Automating Elementary Number-Theoretic Proofs Using Gr\u00f6bner Bases"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1090\/S0894-0347-04-00451-5","volume":"17","author":"M. Aschenbrenner","year":"2004","unstructured":"Aschenbrenner, M.: Ideal membership in polynomial rings over the integers. Journal of the American Mathematical Society\u00a017, 407\u2013441 (2004)","journal-title":"Journal of the American Mathematical Society"},{"key":"5_CR2","volume-title":"A Concise Introduction to the Theory of Numbers","author":"A. Baker","year":"1985","unstructured":"Baker, A.: A Concise Introduction to the Theory of Numbers. Cambridge University Press, Cambridge (1985)"},{"key":"5_CR3","unstructured":"Beltyokov, A.P.: Decidability of the universal theory of natural numbers with addition and divisibility (Russian). Sem. Leningrad Otd. Mat. Inst. Akad. Nauk SSSR 40, 127\u2013130 (1974), English translation in Journal Of Mathematical Sciences 14, 1436\u20131444 (1980)"},{"key":"5_CR4","volume-title":"ACM Monograph Series","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. In: ACM Monograph Series, Academic Press, San Diego (1979)"},{"key":"5_CR5","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, Mathematisches Institut der Universit\u00e4t Innsbruck (1965), English translation to appear in Journal of Symbolic Computation (2006)"},{"key":"5_CR6","first-page":"178","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"A. Bundy","year":"1991","unstructured":"Bundy, A.: A science of reasoning. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, pp. 178\u2013198. MIT Press, Cambridge (1991)"},{"key":"5_CR7","first-page":"91","volume-title":"Machine Intelligence 7","author":"D.C. Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Melzer, B., Michie, D. (eds.) Machine Intelligence 7, pp. 91\u201399. Elsevier, Amsterdam (1972)"},{"key":"5_CR8","volume-title":"An Introduction to the Theory of Numbers","author":"G.H. Hardy","year":"1979","unstructured":"Hardy, G.H., Wright, E.M.: An Introduction to the Theory of Numbers, 5th edn. Clarendon Press, Oxford (1979)","edition":"5"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"5_CR10","first-page":"449","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming (logical foundations)","author":"W. Hodges","year":"1993","unstructured":"Hodges, W.: Logical features of Horn clauses. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming (logical foundations), vol.\u00a01, pp. 449\u2013503. Oxford University Press, Oxford (1993)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/BFb0032842","volume-title":"EUROSAM 1984","author":"A. Kandri-Rody","year":"1984","unstructured":"Kandri-Rody, A., Kapur, D.: Algorithms for computing Gr\u00f6bner bases of polynomial ideals over various Euclidean rings. In: Fitch, J. (ed.) EUROSAM 1984. LNCS, vol.\u00a0174, pp. 195\u2013206. Springer, Heidelberg (1984)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/3-540-15976-2_17","volume-title":"Rewriting Techniques and Applications","author":"A. Kandri-Rody","year":"1985","unstructured":"Kandri-Rody, A., Kapur, D., Narendran, P.: An ideal-theoretic approach to word problems and unification problems over finitely presented commutative algebras. In: Jouannaud, J.-P. (ed.) Rewriting Techniques and Applications. LNCS, vol.\u00a0202, pp. 345\u2013364. Springer, Heidelberg (1985)"},{"key":"5_CR13","unstructured":"Kreisel, G., Krivine, J.-L.: Elements of mathematical logic: model theory. Studies in Logic and the Foundations of Mathematics. North-Holland, revised second edition, 1971. First edition 1967. Translation of the French \u2018El\u00e9ments de logique math\u00e9matique, th\u00e9orie des modeles\u2019 published by Dunod, Paris (1964)"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"89","DOI":"10.2307\/2042394","volume":"79","author":"V. Lifschitz","year":"1980","unstructured":"Lifschitz, V.: Semantical completeness theorems in logic and algebra. Proceedings of the American Mathematical Society\u00a079, 89\u201396 (1980)","journal-title":"Proceedings of the American Mathematical Society"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"271","DOI":"10.2307\/1998219","volume":"235","author":"L. Lipshitz","year":"1978","unstructured":"Lipshitz, L.: The Diophantine problem for addition and divisibility. Transactions of the American Mathematical Society\u00a0235, 271\u2013283 (1978)","journal-title":"Transactions of the American Mathematical Society"},{"key":"5_CR16","first-page":"354","volume":"11","author":"Y.V. Matiyasevich","year":"1970","unstructured":"Matiyasevich, Y.V.: Enumerable sets are Diophantine. Soviet Mathematics Doklady\u00a011, 354\u2013358 (1970)","journal-title":"Soviet Mathematics Doklady"},{"key":"5_CR17","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen In welchem die Addition als einzige Operation hervortritt. In: Sprawozdanie z I Kongresu metematyk\u00f3w slowia\u0144skich, Warszawa 1929, pp. 92\u2013101, 395. Warsaw, 1930. Annotated English version by [20]"},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"98","DOI":"10.2307\/2266510","volume":"14","author":"J. Robinson","year":"1949","unstructured":"Robinson, J.: Definability and decision problems in arithmetic. Journal of Symbolic Logic. Author\u2019s PhD thesis 14, 98\u2013114 (1949)","journal-title":"Journal of Symbolic Logic"},{"key":"5_CR19","doi-asserted-by":"crossref","first-page":"547","DOI":"10.2140\/pjm.1970.34.547","volume":"34","author":"H. Simmons","year":"1970","unstructured":"Simmons, H.: The solution of a decision problem for several classes of rings. Pacific Journal of Mathematics\u00a034, 547\u2013557 (1970)","journal-title":"Pacific Journal of Mathematics"},{"key":"5_CR20","unstructured":"Stansifer, R.: Presburger\u2019s article on integer arithmetic: Remarks and translation. Technical Report CORNELLCS:TR84-639, Cornell University Computer Science Department (1984)"},{"key":"5_CR21","volume-title":"Graduate Texts in Mathematics","author":"V. Weispfenning","year":"1993","unstructured":"Weispfenning, V., Becker, T.: Groebner bases: a computational approach to commutative algebra. In: Graduate Texts in Mathematics, Springer, Heidelberg (1993)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:53:12Z","timestamp":1619502792000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}