{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:41Z","timestamp":1749124061636},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054271","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T03:28:51Z","timestamp":1149650931000},"page":"349-364","source":"Crossref","is-referenced-by-count":14,"title":["Certified version of Buchberger's algorithm"],"prefix":"10.1007","author":[{"given":"Laurent","family":"Th\u00e9ry","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Jacques Calmet and Karsten Homann. Classification of communication and cooperation mechanisms for logical and symbolic computation systems. In First International Workshop \u2018Frontiers of Combining Systems\u2019 (FroCoS'96), Kluwer Series on Applied Logic, pages 133\u2013146. Springer-Verlag, 1996.","DOI":"10.1007\/978-94-009-0349-4_11"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Bruce W. Char, Keith O. Geddes, and Gaston H. Gonnet. First leaves: a tutorial introduction to Maple V. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4615-6996-1"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Edmund Clarke and Xudong Zhao. Analytica \u2014 a theorem prover for Mathematica. Research report, Carnegie Mellon University, 1991.","DOI":"10.1007\/3-540-55602-8_220"},{"key":"32_CR4","unstructured":"Robert L. Constable, Stuart P. Allen, H.M. Bromley, Walter R. Cleaveland, James F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendier, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986."},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Yann Coscoy, Gilles Kahn, and Laurent Th\u00e9ry. Extracting text from proofs. In Typed Lambda Calculus and its Applications, volume 902 of LNCS, pages 109\u2013123. Springer-Verlag, 1995.","DOI":"10.1007\/BFb0014048"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. Little theories. In D. Kapur, editor, Automated Deduction\u2014CADE-11, volume 607 of LNCS, pages 567\u2013581. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_192"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Keith O. Geddes, Stephen R. Czapor, and George Labahn. Algorithms for computer algebra. Kluwer, 1992.","DOI":"10.1007\/b102438"},{"key":"32_CR8","unstructured":"Michael Gordon and Thomas Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"32_CR9","unstructured":"John R. Harrison. Theorem proving with the real numbers. Technical Report 408, University of Cambridge Computer Laboratory, 1996. PhD thesis."},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"John R. Harrison and Laurent Th\u00e9ry. Extending the HOL theorem prover with a computer algebra system to reason about the reals. In Higher Order Logic Theorem Proving and Its Applications, volume 780 of LNCS. Springer-Verlag, August 1995.","DOI":"10.1007\/3-540-57826-9_134"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"Doug Howe. Reasoning About Functional Programs in Nuprl. In Functional Programming, Concurrency, Simulation and Automated Reasoning, volume 693 of LNCS, pages 144\u2013164. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56883-2_9"},{"key":"32_CR12","unstructured":"G\u00e9rard Huet, Gilles Kahn, and Christine Paulin-Mohring. The Coq proof assistant: A tutorial: Version 6.1. Technical Report 204, INRIA, 1997."},{"key":"32_CR13","unstructured":"Paul B. Jackson. Enhancing the Nuprl proof development system and applying it to computational abstract algebra. Technical Report TR95-1509, Cornell University, 1995."},{"key":"32_CR14","unstructured":"Xavier Leroy. Objective Caml. Available at http: \/\/pauillac.inria.fr\/ocaml\/, 1997."},{"key":"32_CR15","unstructured":"Rob P. Nederpelt, J. Herman Geuvers, and Roel C. De Vrijer, editors. Selected papers on Automath. North-Holland, 1994."},{"issue":"5\u20136","key":"32_CR16","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"C. Paulin-Mohring","year":"1993","unstructured":"Christine Paulin-Mohring and Benjamin Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15(5\u20136):607\u2013640, May\u2013June 1993.","journal-title":"Journal of Symbolic Computation"},{"issue":"4","key":"32_CR17","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1016\/S0747-7171(86)80002-5","volume":"2","author":"L. C. Paulson","year":"1986","unstructured":"Lawdrence C. Paulson. Constructing Recursion Operators in Intuitionistic Type Theory. Journal of Symbolic Computation, 2(4):325\u2013355, December 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Isabelle: a generic theorem prover, volume 828 of LNCS. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"32_CR19","unstructured":"Lo\u00cfc Pottier. Dixon's lemma. Available at ftp:\/\/www.inria.fr\/safir\/pottier\/MON\/, 1996."},{"key":"32_CR20","unstructured":"Piotr Rudnicki. An overview of the MIZAR projet. In Workshop on Types and Proofs for Programs. Available by ftp at pub\/csreports\/Bastad92\/proc.ps.Z onftp.cs.chalmers.se, June 1992."},{"key":"32_CR21","unstructured":"John M. Rushby, Natajaran Shankar, and Mandayam Srivas. PVS: Combining specification, proof checking, and model checking. In CAV '96, volume 1102 of LNCS. Springer-Verlag, July 1996."},{"key":"32_CR22","unstructured":"Daniela Vasaru, Tudor Jebelean, and Bruno Buchberger. Theorema: A system for formal scientific training in natural language presentation. Technical Report 97-34, Risc-Linz, 1997."},{"key":"32_CR23","unstructured":"Stephen Wolfram. Mathematica: a system for doing mathematics by computer. Addison-Wesley, 1988."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054271","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,7]],"date-time":"2023-05-07T13:06:54Z","timestamp":1683464814000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054271"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0054271","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}