{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:09Z","timestamp":1747546929121},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_25","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:22:39Z","timestamp":1330251759000},"page":"356-370","source":"Crossref","is-referenced-by-count":2,"title":["Proof script pragmatics in IMPS"],"prefix":"10.1007","author":[{"given":"William M.","family":"Farmer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua D.","family":"Guttman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark E.","family":"Nadel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F. Javier","family":"Thayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"25_CR1","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendier, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"doi-asserted-by":"crossref","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. IMPS: System description. In D. Kapur, editor, Automated Deduction-CADE-11, volume 607 of Lecture Notes in Computer Science, pages 701\u2013705. Springer-Verlag, 1992.","key":"25_CR2","DOI":"10.1007\/3-540-55602-8_207"},{"doi-asserted-by":"crossref","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. Little theories. In D. Kapur, editor, Automated Deduction-CADE-11, volume 607 of Lecture Notes in Computer Science, pages 567\u2013581. Springer-Verlag, 1992.","key":"25_CR3","DOI":"10.1007\/3-540-55602-8_192"},{"key":"25_CR4","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. IMPS: an Interactive Mathematical Proof System. Journal of Automated Reasoning, 11:213\u2013248, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR5","volume-title":"Technical Report M93B-138","author":"W. M. Farmer","year":"1993","unstructured":"W. M. Farmer, J. D. Guttman, and F. J. Thayer. The IMPS user's manual. Technical Report M93B-138, The MITRE Corporation, Bedford, MA, November 1993."},{"doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.","key":"25_CR6","DOI":"10.1007\/3-540-09724-4"},{"doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P. A. Surahmanyam, editors, VLSI Specification, Verification, and Synthesis, pages 73\u2013128. Kluwer, 1987.","key":"25_CR7","DOI":"10.1007\/978-1-4613-2007-4_3"},{"unstructured":"R. Milner. The use of machines to assist in rigorous proof. In C A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 77\u201388. Prentice\/Hall International, 1985.","key":"25_CR8"},{"unstructured":"L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361-368. Academic Press, 1990.","key":"25_CR9"},{"unstructured":"J. A. Rees, N. I. Adams, and J. R. Meehan. The T Manual. Computer Science Department, Yale University, fifth edition, 1988.","key":"25_CR10"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:17:35Z","timestamp":1605629855000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}