{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:22:43Z","timestamp":1725664963291},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617327"},{"type":"electronic","value":"9783540707400"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61732-9_48","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:17:03Z","timestamp":1330294623000},"page":"21-37","source":"Crossref","is-referenced-by-count":1,"title":["Analytica \u2014 An experiment in combining theorem proving and symbolic computation"],"prefix":"10.1007","author":[{"given":"Andrej","family":"Bauer","sequence":"first","affiliation":[]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[]},{"given":"Xudong","family":"Zhao","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BF00248320","volume":"5","author":"P. B. Andrews","year":"1989","unstructured":"P. B. Andrews. On connections and higher-order logic. Journal of Automated Reasoning, 5:257\u2013291, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"B. C. Berndt. Ramanujan's Notebooks, Part I. Springer-Verlag, 1985.","DOI":"10.1007\/978-1-4612-1088-7"},{"key":"2_CR3","volume-title":"Technical Report ATP-17B","author":"W. W. Bledsoe","year":"1983","unstructured":"W. W. Bledsoe. The ut natural deduction prover. Technical Report ATP-17B, Mathematical Dept., University of Texas at Austin, 1983."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"W. W. Bledsoe. Some automatic proofs in analysis. In Automated Theorem Proving: After 25 Years. American Mathematical Society, 1984.","DOI":"10.1090\/conm\/029\/06"},{"key":"2_CR5","volume-title":"Technical Report ATP-40A","author":"W. W. Bledsoe","year":"1979","unstructured":"W. W. Bledsoe, P. Bruell, and R. E. Shostak. A prover for general inequalities. Technical Report ATP-40A, Mathematical Dept., University of Texas at Austin, 1979."},{"key":"2_CR6","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, 1979."},{"key":"2_CR7","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Technical report, Department of Artificial Intelligence, University of Edinburgh, 1988."},{"key":"2_CR8","unstructured":"E. M. Clarke and X. Zhao. Analytica: A theorem prover for mathematica. The Journal of Mathematica, 3(1), 1993."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. Imps: An interactive mathematical proof system. Technical report, The MITRE Corporation, 1990.","DOI":"10.21236\/ADA243162"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"M. Fitting. First-order Logic and Automated Theorem Proving. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"2_CR11","unstructured":"J. H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, 1986."},{"key":"2_CR12","unstructured":"M. Gorden. Hol: A machine oriented formulation of higher order logic. Technical report, Computer Laboratory, University of Cambridge, 1985."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"M. Gorden, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanised logic of computation, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"2_CR14","unstructured":"R. W. Gosper. Indefinite hypergeometric sums in macsyma. In Proceedings of the MACSYMA Users Conference, pages 237\u2013252, 1977."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"R. L. London and D. R. Musser. The application of a symbolic mathematical system to program verification. Technical report, USC Information Science Institute, 1975.","DOI":"10.1145\/800182.810412"},{"key":"2_CR16","volume-title":"Technical report","author":"A. Quaife","year":"1989","unstructured":"A. Quaife. Automated deduction in von neumann-bernays-godel set theory. Technical report, Dept. of Mathematics, Univ. of California at Berkeley, 1989."},{"key":"2_CR17","unstructured":"E. Sacks. Hierarchical inequality reasoning. Technical report, MIT Laboratory for Computer Science, 1987."},{"key":"2_CR18","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1016\/S0747-7171(89)80041-0","volume":"7","author":"P. Suppes","year":"1989","unstructured":"P. Suppes and S. Takahashi. An interactive calculus theorem-prover for continuity properties. Journal of Symbolic Computation, 7:573\u2013590, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR19","unstructured":"S. Wolfram. Mathematica: A System for Doing Mathematics by Computer. Wolfram Research Inc., 1988."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Mathematical Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61732-9_48.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:09:48Z","timestamp":1605647388000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61732-9_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617327","9783540707400"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-61732-9_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}