{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:14:29Z","timestamp":1753888469089,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":45,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642323461"},{"type":"electronic","value":"9783642323478"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32347-8_24","type":"book-chapter","created":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T11:33:54Z","timestamp":1344598434000},"page":"345-360","source":"Crossref","is-referenced-by-count":13,"title":["More SPASS with Isabelle"],"prefix":"10.1007","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Wand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E. Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition Modulo Linear Arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 84\u201399. Springer, Heidelberg (2009)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M. Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A Modular Integration of SAT\/SMT Solvers to COQ through Proof Witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol.\u00a07086, pp. 135\u2013150. Springer, Heidelberg (2011)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"issue":"3-4","key":"24_CR4","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. J.\u00a0Autom. Reas.\u00a029(3-4), 253\u2013275 (2002)","journal-title":"J.\u00a0Autom. Reas."},{"key":"24_CR5","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT Solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 116\u2013130. Springer, Heidelberg (2011)"},{"key":"24_CR6","unstructured":"Blanchette, J.C., B\u00f6hme, S., Smallbone, N.: Monotonicity or how to encode polymorphic types safely and efficiently, http:\/\/www21.in.tum.de\/~blanchet\/mono-trans.pdf"},{"key":"24_CR7","unstructured":"Blanchette, J.C., Paskevich, A.: TFF1: The TPTP typed first-order form with rank-1 polymorphism, http:\/\/www21.in.tum.de\/~blanchet\/tff1spec.pdf"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Bobot, F., Conchon, S., Contejean, E., Lescuyer, S.: Implementing polymorphism in SMT solvers. In: Barrett, C., de Moura, L. (eds.) SMT 2008, pp. 1\u20135. ICPS, ACM (2008)","DOI":"10.1145\/1512464.1512466"},{"key":"24_CR9","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-24364-6_7","volume-title":"Frontiers of Combining Systems","author":"F. Bobot","year":"2011","unstructured":"Bobot, F., Paskevich, A.: Expressing Polymorphic Types in a Many-Sorted Language. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol.\u00a06989, pp. 87\u2013102. Springer, Heidelberg (2011)"},{"key":"24_CR10","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol.\u00a06173, pp. 107\u2013121. Springer, Heidelberg (2010)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-Style Proof Reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 179\u2013194. Springer, Heidelberg (2010)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A Practical System for Verifying Concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"24_CR13","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-24364-6_9","volume-title":"Frontiers of Combining Systems","author":"A. Eggers","year":"2011","unstructured":"Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., Weidenbach, C.: Superposition Modulo Non-linear Arithmetic. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol.\u00a06989, pp. 119\u2013134. Springer, Heidelberg (2011)"},{"key":"24_CR14","unstructured":"Filli\u00e2tre, J.C.: Private Communication (March 2012)"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/3-540-63104-6_32","volume-title":"Automated Deduction - CADE-14","author":"H. Ganzinger","year":"1997","unstructured":"Ganzinger, H., Meyer, C., Weidenbach, C.: Soft Typing for Ordered Resolution. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 321\u2013335. Springer, Heidelberg (1997)"},{"issue":"11","key":"24_CR16","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof\u2014The four-color theorem. N. AMS\u00a055(11), 1382\u20131393 (2008)","journal-title":"N. AMS"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/978-3-642-24559-6_41","volume-title":"Formal Methods and Software Engineering","author":"W. Guttmann","year":"2011","unstructured":"Guttmann, W., Struth, G., Weber, T.: Automating Algebraic Methods in Isabelle. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 617\u2013632. Springer, Heidelberg (2011)"},{"key":"24_CR18","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":"24_CR19","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Mu\u00f1oz, C. (eds.) Design and Application of Strategies\/Tactics in Higher Order Logics, pp. 56\u201368, No. CP-2003-212448 in NASA Technical Reports (2003)"},{"issue":"6","key":"24_CR20","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G. Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an operating-system kernel. C. ACM\u00a053(6), 107\u2013115 (2010)","journal-title":"C. ACM"},{"key":"24_CR21","unstructured":"Klein, G., Nipkow, T., Paulson, L. (eds.): The Archive of Formal Proofs, http:\/\/afp.sf.net\/"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"issue":"4","key":"24_CR23","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reas.\u00a043(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reas."},{"key":"24_CR24","unstructured":"Leroy, X.: Private Communication (October 2011)"},{"key":"24_CR25","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/10721959_30","volume-title":"Automated Deduction - CADE-17","author":"W. McCune","year":"2000","unstructured":"McCune, W., Shumsky, O.: System Description: IVY. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831, pp. 401\u2013405. Springer, Heidelberg (2000)"},{"issue":"2","key":"24_CR26","first-page":"43","volume":"144","author":"S. McLaughlin","year":"2006","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. ENTCS\u00a0144(2), 43\u201351 (2006)","journal-title":"ENTCS"},{"issue":"1","key":"24_CR27","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J. Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J.\u00a0Autom. Reas.\u00a040(1), 35\u201360 (2008)","journal-title":"J.\u00a0Autom. Reas."},{"issue":"1","key":"24_CR28","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J. Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic\u00a07(1), 41\u201357 (2009)","journal-title":"J. Applied Logic"},{"key":"24_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"24_CR30","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: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"24_CR31","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a\u00a0practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) IWIL 2010 (2010)"},{"key":"24_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-540-74591-4_18","volume-title":"Theorem Proving in Higher Order Logics","author":"L.C. Paulson","year":"2007","unstructured":"Paulson, L.C., Susanto, K.W.: Source-Level Proof Reconstruction for Interactive Theorem Proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 232\u2013245. Springer, Heidelberg (2007)"},{"key":"24_CR33","unstructured":"Popescu, A., H\u00f6lzl, J., Nipkow, T.: Proving possibilistic, probabilistic noninterference, http:\/\/www21.in.tum.de\/~popescua\/pos.pdf (submitted)"},{"issue":"2-3","key":"24_CR34","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Comm.\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Comm."},{"key":"24_CR35","unstructured":"Rudnicki, P., Urban, J.: Escape to ATP for Mizar. In: Fontaine, P., Stump, A. (eds.) PxTP 2011 (2011)"},{"key":"24_CR36","doi-asserted-by":"crossref","unstructured":"Rushby, J.M.: Tutorial: Automated formal methods with PVS, SAL, and Yices. In: Hung, D.V., Pandya, P. (eds.) SEFM 2006, p. 262. IEEE (2006)","DOI":"10.1109\/SEFM.2006.37"},{"issue":"1","key":"24_CR37","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Comm.\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE J. Sel. Areas Comm."},{"key":"24_CR38","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-25984-8_15","volume-title":"Automated Reasoning","author":"S. Schulz","year":"2004","unstructured":"Schulz, S.: System Description: E\u00a00.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 223\u2013228. Springer, Heidelberg (2004)"},{"key":"24_CR39","doi-asserted-by":"crossref","unstructured":"Siekmann, J., Benzm\u00fcller, C., Fiedler, A., Meier, A., Normann, I., Pollet, M.: Proof development with \u03a9mega: The irrationality of $\\sqrt2$ . In: Kamareddine, F. (ed.) Thirty Five Years of Automating Mathematics. Applied Logic, vol.\u00a028, pp. 271\u2013314. Springer, Heidelberg (2003)","DOI":"10.1007\/978-94-017-0253-9_11"},{"issue":"4","key":"24_CR40","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure\u2014The FOF and CNF parts, v3.5.0. J. Autom. Reas.\u00a043(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reas."},{"issue":"1","key":"24_CR41","doi-asserted-by":"crossref","first-page":"49","DOI":"10.3233\/AIC-2012-0512","volume":"25","author":"G. Sutcliffe","year":"2012","unstructured":"Sutcliffe, G.: The CADE-23 automated theorem proving system competition\u2014CASC-23. AI Comm.\u00a025(1), 49\u201363 (2012)","journal-title":"AI Comm."},{"key":"24_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-642-28717-6_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Sutcliffe","year":"2012","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP Typed First-Order Form with Arithmetic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 406\u2013419. Springer, Heidelberg (2012)"},{"key":"24_CR43","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0II, pp. 1965\u20132013. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"key":"24_CR44","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C. Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol.\u00a05663, pp. 140\u2013145. Springer, Heidelberg (2009)"},{"issue":"4","key":"24_CR45","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"Wos, L., Robinson, G.A., Carson, D.F.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM\u00a012(4), 536\u2013541 (1965)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32347-8_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T19:26:00Z","timestamp":1743967560000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32347-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642323461","9783642323478"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32347-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}