{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T03:52:19Z","timestamp":1768449139327,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540223450","type":"print"},{"value":"9783540259848","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-25984-8_28","type":"book-chapter","created":{"date-parts":[[2010,9,11]],"date-time":"2010-09-11T02:31:38Z","timestamp":1284172298000},"page":"372-384","source":"Crossref","is-referenced-by-count":8,"title":["Experiments on Supporting Interactive Proof Using Resolution"],"prefix":"10.1007","author":[{"given":"Jia","family":"Meng","sequence":"first","affiliation":[]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-94-017-0435-9_4","volume-title":"Automated Deduction\u2014 A Basis for Applications, Systems and Implementation Techniques","author":"W. Ahrendt","year":"1998","unstructured":"Ahrendt, W., Beckert, B., H\u00e4hnle, R., Menzel, W., Reif, W., Schellhorn, G., Schmitt, P.H.: Integrating automated and interactive theorem proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction\u2014 A Basis for Applications, Systems and Implementation Techniques, vol.\u00a0II, pp. 97\u2013116. Kluwer Academic Publishers, Dordrecht (1998)"},{"issue":"3-4","key":"28_CR2","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M. Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D., de Nivelle, H.: Automatic proof construction in type theory using resolution. Journal of Automated Reasoning\u00a029(3-4), 253\u2013275 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR3","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.-L. Chang","year":"1973","unstructured":"Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, London (1973)"},{"key":"28_CR4","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":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 311\u2013321. Springer, Heidelberg (1999)"},{"key":"28_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-45620-1_10","volume-title":"Automated Deduction - CADE-18","author":"J. Hurd","year":"2002","unstructured":"Hurd, J.: An LCF-style interface between HOL and first-order logic. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 134\u2013138. Springer, Heidelberg (2002)"},{"key":"28_CR7","unstructured":"Meng, J.: Integration of interactive and automatic provers. In: Carro, M., Correas, J. (eds.) Second CologNet Workshop on Implementation Technology for Computational Logic Systems (2003), On the Internet at http:\/\/www.cl.cam.ac.uk\/users\/jm318\/papers\/integration.pdf"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson and Voronkov [17], ch. 6. pp. 335\u2013367","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"28_CR11","volume-title":"Automated Reasoning and its Applications: Essays in Honor of Larry Wos","author":"L.C. Paulson","year":"1997","unstructured":"Paulson, L.C.: Generic automatic proof tools. In: Veroff, R. (ed.) Automated Reasoning and its Applications: Essays in Honor of Larry Wos, ch. 3. MIT Press, Cambridge (1997)"},{"key":"28_CR12","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"issue":"3","key":"28_CR13","first-page":"73","volume":"5","author":"L.C. Paulson","year":"1999","unstructured":"Paulson, L.C.: A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science\u00a05(3), 73\u201387 (1999)","journal-title":"Journal of Universal Computer Science"},{"key":"28_CR14","unstructured":"Paulson, L.C.: Isabelle\u2019s isabelle\u2019s logics: FOL and ZF. Technical report, Computer Laboratory, University of Cambridge (2003), On the Internet at http:\/\/isabelle.in.tum.de\/dist\/Isabelle2003\/doc\/logics-ZF.pdf"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Riazanov, A., Voronkov, A.: Efficient checking of term ordering constraints. Preprint CSPP-21, Department of Computer Science, University of Manchester (February 2003)","DOI":"10.1007\/978-3-540-25984-8_3"},{"key":"28_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-45744-5_29","volume-title":"Automated Reasoning","author":"A. Riazanov","year":"2001","unstructured":"Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 376\u2013380. Springer, Heidelberg (2001)"},{"key":"28_CR17","volume-title":"Handbook of Automated Reasoning","year":"2001","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier Science, Amsterdam (2001)"},{"key":"28_CR18","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-94-017-0253-9_11","volume-title":"Thirty Five Years of Automating Mathematics","author":"J. Siekmann","year":"2003","unstructured":"Siekmann, J., Benzm\u00fcller, C., Fiedler, A., Meier, A., Normann, I., Pollet, M.: Proof development with \u03c9mega: The irrationality of $\\sqrt{2}$ . In: Kamareddine, F. (ed.) Thirty Five Years of Automating Mathematics, pp. 271\u2013314. Kluwer Academic Publishers, Dordrecht (2003)"},{"issue":"2","key":"28_CR19","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson and Voronkov [17], ch. 27. pp. 1965\u20132013","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 307\u2013322. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-25984-8_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:18:55Z","timestamp":1605759535000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-25984-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223450","9783540259848"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-25984-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}