{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171773},"publisher-location":"Berlin\/Heidelberg","reference-count":3,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012891","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T01:12:39Z","timestamp":1132708359000},"page":"772-773","source":"Crossref","is-referenced-by-count":10,"title":["Isabelle: The next seven hundred theorem provers"],"prefix":"10.1007","author":[{"given":"Lawrence C","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"72_CR1","doi-asserted-by":"crossref","unstructured":"L. C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF (Cambridge University Press, 1987).","DOI":"10.1017\/CBO9780511526602"},{"key":"72_CR2","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"L. C. Paulson","year":"1986","unstructured":"L. C. Paulson, Natural deduction as higher-order resolution, Journal of Logic Programming\n3 (1986), pages 237\u2013258.","journal-title":"Journal of Logic Programming"},{"key":"72_CR3","unstructured":"L. C. Paulson, Higher-order logic as the basis of generic theorem provers, Report, Computer Lab., University of Cambridge (1988)."}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012891.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T10:06:51Z","timestamp":1607335611000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012891"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":3,"URL":"https:\/\/doi.org\/10.1007\/bfb0012891","relation":{},"subject":[]}}