{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:20:05Z","timestamp":1725567605163},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_40","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T08:51:59Z","timestamp":1286182319000},"page":"565-580","source":"Crossref","is-referenced-by-count":1,"title":["An Isabelle-Like Procedural Mode for HOL Light"],"prefix":"10.1007","author":[{"given":"Petros","family":"Papapanagiotou","sequence":"first","affiliation":[]},{"given":"Jacques","family":"Fleuriot","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"40_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/11532231_22","volume-title":"Automated Deduction \u2013 CADE-20","author":"S. McLaughlin","year":"2005","unstructured":"McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 295\u2013314. Springer, Heidelberg (2005)"},{"key":"40_CR2","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. Loveland","year":"1968","unstructured":"Loveland, D.: Mechanical Theorem-Proving by Model Elimination. Journal of the ACM (JACM)\u00a015, 236\u2013251 (1968)","journal-title":"Journal of the ACM (JACM)"},{"key":"40_CR3","volume-title":"Logic and computation: interactive proof with Cambridge LCF","author":"L. Paulson","year":"1990","unstructured":"Paulson, L.: Logic and computation: interactive proof with Cambridge LCF. Cambridge Univ. Pr., Cambridge (1990)"},{"key":"40_CR4","unstructured":"Prawitz, D.: Natural deduction: A proof-theoretical study. Almqvist & Wiksell Stockholm (1965)"},{"key":"40_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"40_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/3-540-61511-3_97","volume-title":"Automated Deduction - Cade-13","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 313\u2013327. Springer, Heidelberg (1996)"},{"key":"40_CR7","unstructured":"Harrison, J.: HOL Light: future wishes. In: Talk at Workshop on Interactive Theorem Proving, Cambridge (2009), \n                  \n                    http:\/\/www.cl.cam.ac.uk\/~jrh13\/slides\/itp-25aug09\/slides.pdf"},{"key":"40_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle.: Generic Theorem Prover","author":"L. Paulson","year":"1994","unstructured":"Paulson, L.: Isabelle.: Generic Theorem Prover. Springer, Heidelberg (1994)"},{"key":"40_CR9","first-page":"73","volume":"5","author":"L. Paulson","year":"1999","unstructured":"Paulson, L.: A generic tableau prover and its integration with Isabelle. J. UCS\u00a05, 73\u201387 (1999)","journal-title":"J. UCS"},{"key":"40_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic. Springer, Heidelberg (2002)"},{"key":"40_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 377\u2013440. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T10:05:25Z","timestamp":1553162725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}