{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:43:49Z","timestamp":1725489829135},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540746201"},{"type":"electronic","value":"9783540746218"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74621-8_6","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T11:46:32Z","timestamp":1187783192000},"page":"88-102","source":"Crossref","is-referenced-by-count":1,"title":["A Compressing Translation from Propositional Resolution to Natural Deduction"],"prefix":"10.1007","author":[{"given":"Hasan","family":"Amjad","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","first-page":"210","volume-title":"FOCS","author":"M. Alekhnovich","year":"2001","unstructured":"Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. In: FOCS, pp. 210\u2013219. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 167\u2013181. Springer, Heidelberg (2006)"},{"key":"6_CR3","volume-title":"Introduction to HOL : A theorem-proving environment for higher order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A theorem-proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"6_CR4","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI International (1995)"},{"key":"6_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":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/BFb0105407","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: St\u00e5lmarck\u2019s algorithm as a HOL derived rule. In: von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 221\u2013234. Springer, Heidelberg (1996)"},{"key":"6_CR7","unstructured":"Huet, G., Kahn, G., Paulin-Mohring, C.: The Coq proof assistant: A tutorial: Version 7.2. Technical Report RT-0256, INRIA (February 2002)"},{"key":"6_CR8","unstructured":"Mitchell, D.G.: A SAT solver primer. In: EATCS Bulletin (The Logic in Computer Science Column), vol. 85, pp. 112\u2013133 (February 2005)"},{"issue":"4","key":"6_CR9","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1145\/321479.321481","volume":"15","author":"D.R. Morrison","year":"1968","unstructured":"Morrison, D.R.: PATRICIA-Practical Algorithm To Retrieve Information Code. In Alphanumeric. J. ACM\u00a015(4), 514\u2013534 (1968)","journal-title":"In Alphanumeric. J. ACM"},{"key":"6_CR10","first-page":"530","volume-title":"Proceedings of the 38th Design Automation Conference","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, pp. 530\u2013535. ACM Press, New York (2001)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"CADE 1992","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: A Generic Theorem Prover. In: Paulson, L.C. (ed.) Isabelle. LNCS, vol.\u00a0828, Springer, Heidelberg (1994)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/3-540-44755-5_3","volume-title":"Theorem Proving in Higher Order Logics","author":"N. Shankar","year":"2001","unstructured":"Shankar, N.: Using decision procedures with a higher-order logic. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 5\u201326. Springer, Heidelberg (2001)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Sinz, C.: Compressing propositional proofs by common subproof extraction. In: Pichler, F. (ed.) Euro Conference on Computer Aided Systems Theory (2007)","DOI":"10.1007\/978-3-540-75867-9_69"},{"issue":"3","key":"6_CR15","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/BF01206331","volume":"14","author":"E. Ukkonen","year":"1995","unstructured":"Ukkonen, E.: Online construction of suffix trees. Algorithmica\u00a014(3), 249\u2013260 (1995)","journal-title":"Algorithmica"},{"key":"6_CR16","unstructured":"Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers.JAL (special issue on Empirically Successful Computerized Reasoning) (to appear, 2007)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74621-8_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:30:43Z","timestamp":1619519443000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74621-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540746201","9783540746218"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74621-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}