{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:37:05Z","timestamp":1725467825548},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649601"},{"type":"electronic","value":"9783540498162"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055903","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T17:17:34Z","timestamp":1154020654000},"page":"67-83","source":"Crossref","is-referenced-by-count":6,"title":["Automatic generation of epsilon-delta proofs of continuity"],"prefix":"10.1007","author":[{"given":"Michael","family":"Beeson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Beeson, M.: Logic and computation in Mathpert: an expert system for learning mathematics, in: Kaltofen, E., and Watt, S. M. (eds.), Computers and Mathematics, pp. 202\u2013214, Springer-Verlag (1989).","DOI":"10.1007\/978-1-4613-9647-5_25"},{"key":"6_CR2","volume-title":"Human Interfaces to Symbolic Computation","author":"M. Beeson","year":"1996","unstructured":"Beeson, M.: Design Principles of Mathpert: Software to support education in algebra and calculus, in: Kajler, N. (ed.) Human Interfaces to Symbolic Computation, Springer-Verlag, Berlin\/Heidelberg\/New York (1996)."},{"issue":"3","key":"6_CR3","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1142\/S0129054195000172","volume":"6","author":"M. Beeson","year":"1995","unstructured":"Beeson, M.: Using nonstandard analysis to ensure the correctness of symbolic computations, International Journal of Foundations of Computer Science\n                        6(3) (1995) 299\u2013338.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Beeson, M.: Some applications of Gentzen\u2019s proof theory in automated deduction, in: Shroeder-Heister, P., Extensions of Logic Programming, Springer Lecture Notes in Computer Science 475, pp. 101\u2013156, Springer-Verlag (1991).","DOI":"10.1007\/BFb0038693"},{"key":"6_CR5","volume-title":"Unification in lambda-calculus","author":"M. Beeson","year":"1998","unstructured":"Beeson, M.: Unification in lambda-calculus, to appear in Automated Deduction: CADE-15 \u2014 Proc. of the 15th International Conference on Automated Deduction, Springer-Verlag, Berlin\/Heidelberg (1998)."},{"key":"6_CR6","series-title":"volume 29 in the Contemporary Mathematics series","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1090\/conm\/029\/06","volume-title":"Automoated Theorem Proving: After 25 Years","author":"W. W. Bledsoe","year":"1984","unstructured":"Bledsoe, W. W.: Some automatic proofs in analysis, pp. 89\u2013118 in: W. Bledsoe and D. Loveland (eds.) Automoated Theorem Proving: After 25 Years, volume 29 in the Contemporary Mathematics series, AMS, Providence, R. I. (1984)."},{"key":"6_CR7","unstructured":"Boyer, R., and Moore, J.: A Computational Logic, Academic Press (1979)."},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(87)80020-2","volume":"3","author":"B. Buchberger","year":"1987","unstructured":"Buchberger, B.: History and basic features of the critical-pair completeion procedure, J. Symbolic Computation\n                        3:3\u201388 (1987).","journal-title":"J. Symbolic Computation"},{"key":"6_CR9","first-page":"761","volume-title":"Analytica: A Theorem Prover in Mathematica","author":"E. Clarke","year":"1992","unstructured":"Clarke, E., and Zhao, X.: Analytica: A Theorem Prover in Mathematica, in: Kapur, D. (ed.), Automated Deduction: CADE-11 \u2014 Proc. of the 11th International Conference on Automated Deduction, pp. 761\u2013765, Springer-Verlag, Berlin\/Heidelberg (1992)."},{"key":"6_CR10","volume-title":"Algorithms in Real Algebraic Geometry","author":"M. Coste","year":"1988","unstructured":"Coste, M., and Roy, M. F.: Thom\u2019s lemma, the coding of real algebraic numbers, and the computation of the topology of semi-algebraic sets, in: Arnon, D. S., and Buchberger, B., Algorithms in Real Algebraic Geometry, Academic Press, London (1988)."},{"key":"6_CR11","unstructured":"Harrison, J., and Thery, L.: Extending the HOL theorem prover with a computer algebra system to reason about the reals, in Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG \u201993, pp. 174\u2013184, Lecture Notes in Computer Science 780, Springer-Verlag (1993)."},{"key":"6_CR12","volume-title":"Introduction to Metamathematics","author":"S. C. Kleene","year":"1952","unstructured":"Kleene, S. C., Introduction to Metamathematics, van Nostrand, Princeton, N. J. (1952)."},{"key":"6_CR13","first-page":"663","volume-title":"Otter 2.0","author":"W. McCune","year":"1990","unstructured":"McCune, W.: Otter 2.0, in: Stickel, M. E. (ed.), 10th International Conference on Automated Deduction pp. 663\u2013664, Springer-Verlag, Berlin\/Heidelberg (1990)."},{"key":"6_CR14","first-page":"511","volume":"33","author":"D. Richardson","year":"1968","unstructured":"Richardson, D., Some unsolvable problems involving elementary functions of a real variable, J. Symbolic Logic 33 511\u2013520 (1968).","journal-title":"J. Symbolic Logic"},{"issue":"7","key":"6_CR15","first-page":"779","volume":"38","author":"R. Stoutemeyer","year":"1991","unstructured":"Stoutemeyer, R.: Crimes and misdemeanors in the computer algebra trade, Notices of the A.M.S\n                        38(7) 779\u2013785, September 1991.","journal-title":"Notices of the A.M.S"},{"key":"6_CR16","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/BF02328447","volume":"2","author":"W. Wen-Tsum","year":"1986","unstructured":"Wu Wen-Tsum: Basic principles of mechanical theorem-proving in elementary geometries, J. Automated Reasoning\n                        2 221\u2013252, 1986.","journal-title":"J. Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055903","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T13:55:14Z","timestamp":1549893314000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055903"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649601","9783540498162"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0055903","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}