{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:04Z","timestamp":1749125404216,"version":"3.41.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1998,12,1]],"date-time":"1998-12-01T00:00:00Z","timestamp":912470400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,12,1]],"date-time":"1998-12-01T00:00:00Z","timestamp":912470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1998,12]]},"DOI":"10.1023\/a:1006079212546","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:38:24Z","timestamp":1040517504000},"page":"295-325","source":"Crossref","is-referenced-by-count":21,"title":["Analytica \u2013 An Experiment in Combining Theorem Proving and Symbolic Computation"],"prefix":"10.1007","volume":"21","author":[{"given":"Andrej","family":"Bauer","sequence":"first","affiliation":[]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[]},{"given":"Xudong","family":"Zhao","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"181212_CR1","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF02341853","volume":"8","author":"D. Baker-Plummer","year":"1992","unstructured":"Baker-Plummer, D.: Gazing: An approach to the problem of definition and lemma use, J. Automated Reasoning\n8 (1992), 311\u2013344.","journal-title":"J. Automated Reasoning"},{"key":"181212_CR2","doi-asserted-by":"crossref","unstructured":"Ballarin, C., Homann, K., and Calmet, J.: Theorems and algorithms: An interface between Isabelle and Maple, in Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation, July 1995, Montreal, Canada.","DOI":"10.1145\/220346.220366"},{"key":"181212_CR3","doi-asserted-by":"crossref","unstructured":"Berndt, B. C.: Ramanujan's Notebooks, Part I, Springer-Verlag, 1985.","DOI":"10.1007\/978-1-4612-1088-7"},{"key":"181212_CR4","series-title":"Technical Report","volume-title":"The UT natural deduction prover","author":"W. W. Bledsoe","year":"1983","unstructured":"Bledsoe, W. W.: The UT natural deduction prover, Technical Report ATP-17B, Mathematical Dept., University of Texas at Austin, 1983."},{"key":"181212_CR5","doi-asserted-by":"crossref","unstructured":"Bledsoe, W. W.: Some automatic proofs in analysis, in Automated Theorem Proving: After 25 Years, American Mathematical Society, 1984.","DOI":"10.1090\/conm\/029"},{"key":"181212_CR6","series-title":"Technical Report","volume-title":"A prover for general inequalities","author":"W. W. Bledsoe","year":"1979","unstructured":"Bledsoe, W. W., Bruell, P., and Shostak, R.: A prover for general inequalities, Technical Report ATP-40A, Mathematical Dept., University of Texas at Austin, 1979."},{"key":"181212_CR7","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic, Academic Press, 1979."},{"key":"181212_CR8","unstructured":"Bundy, A., van Harmelen, F., Hesketh, J., and Smaill, A.: Experiments with proof plans for induction, Technical report, Department of Artificial Intelligence, University of Edinburgh, 1988."},{"key":"181212_CR9","unstructured":"Clarke, E. M. and Zhao, X.: Combining symbolic computation and theorem proving: Some problems of Ramanujan, in Proceedings of 11th International Conference on Automated Deduction, 1992."},{"key":"181212_CR10","unstructured":"Clarke, E. M. and Zhao, X.: Analytica: A theorem prover for Mathematica, J. Math.\n3(1) (1993)."},{"key":"181212_CR11","doi-asserted-by":"crossref","unstructured":"Farmer, W. M., Guttman, J. D., and Thayer, F. J.: IMPS: An interactive mathematical proof system, Technical Report, The MITRE Corporation, 1990.","DOI":"10.21236\/ADA243162"},{"key":"181212_CR12","doi-asserted-by":"crossref","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"181212_CR13","unstructured":"Gallier, J. H.: Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper & Row, 1986."},{"key":"181212_CR14","unstructured":"Gordon, M.: HOL: A machine oriented formulation of higher order logic, Technical Report, Computer Laboratory, University of Cambridge, 1985."},{"key":"181212_CR15","doi-asserted-by":"crossref","unstructured":"Gordon, M., Milner, R., and Wadsworth, C.: Edinburgh LCF: A mechanised logic of computation, in Lecture Notes in Comput. Sci. 78, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"181212_CR16","unstructured":"Gosper, R. W.: Indefinite hypergeometric sums in MACSYMA, in Proceedings of the MACSYMA Users Conference, 1977, pp. 237\u2013252."},{"key":"181212_CR17","doi-asserted-by":"crossref","unstructured":"Harrison, J. and Th\u00e9ry, L.: Extending HOL theorem prover with a computer algebra system to reason about the reals, in J. J. Joyce and C. Seger (eds), Proceedings of Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Comput. Sci. 780, Springer-Verlag, 1994.","DOI":"10.1007\/3-540-57826-9_134"},{"key":"181212_CR18","unstructured":"London, R. L. and Musser, D. R.: The application of a symbolic mathematical system to program verification, Technical Report, Information Science Institute, University of Southern California, 1975."},{"key":"181212_CR19","volume-title":"Automated deduction in von Neumann\u2013Bernays\u2013G\u00f6del set theory","author":"A. Quaife","year":"1989","unstructured":"Quaife, A.: Automated deduction in von Neumann\u2013Bernays\u2013G\u00f6del set theory, Technical Report, Dept. of Mathematics, University of California at Berkeley, 1989."},{"key":"181212_CR20","unstructured":"Sacks, E.: Hierarchical inequality reasoning, Technical Report, MIT Laboratory for Computer Science, 1987."},{"key":"181212_CR21","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1016\/S0747-7171(89)80041-0","volume":"7","author":"P. Suppes","year":"1989","unstructured":"Suppes, P. and Takahashi, S.: An interactive calculus theorem-prover for continuity properties, J. Symbolic Comput.\n7 (1989), 573\u2013590.","journal-title":"J. Symbolic Comput."},{"key":"181212_CR22","unstructured":"Titchmarsh, E. C.: The Theory of Functions, Oxford University Press, 1932."},{"key":"181212_CR23","unstructured":"Wolfram, S.: Mathematica: A System for Doing Mathematics by Computer, Wolfram Research Inc., 1988."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006079212546.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006079212546\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006079212546.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:39:56Z","timestamp":1749123596000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006079212546"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,12]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1998,12]]}},"alternative-id":["181212"],"URL":"https:\/\/doi.org\/10.1023\/a:1006079212546","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,12]]}}}