{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:05Z","timestamp":1749124085859},"publisher-location":"Berlin, Heidelberg","reference-count":4,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_220","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:22:38Z","timestamp":1330251758000},"page":"761-765","source":"Crossref","is-referenced-by-count":17,"title":["Analytica \u2014 A theorem prover in mathematica"],"prefix":"10.1007","author":[{"given":"Edmund","family":"Clarke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xudong","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"70_CR1","doi-asserted-by":"crossref","unstructured":"B.C.Berndt, Ramanujan's Notebooks, Part I, Springer-Verlag, 1985, pp 25\u201343.","DOI":"10.1007\/978-1-4612-1088-7_3"},{"key":"70_CR2","unstructured":"R.W.Gosper, Indefinite Hypergeometric sums in MACSYMA."},{"key":"70_CR3","unstructured":"E.Sacks, Hierarchical Inequality Reasoning, Technique Report, MIT Laboratory for Computer Science, 1987."},{"key":"70_CR4","unstructured":"S. Wolfram. Mathematica: A System for Doing Mathematics by Computer, Wolfram Research Inc., 1988."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_220.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:00:28Z","timestamp":1605646828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_220"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":4,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_220","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}