{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T01:25:30Z","timestamp":1725585930266},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642221187"},{"type":"electronic","value":"9783642221194"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22119-4_21","type":"book-chapter","created":{"date-parts":[[2011,6,15]],"date-time":"2011-06-15T14:21:08Z","timestamp":1308147668000},"page":"263-277","source":"Crossref","is-referenced-by-count":29,"title":["MaLeCoP Machine Learning Connection Prover"],"prefix":"10.1007","author":[{"given":"Josef","family":"Urban","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"Vysko\u010dil","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"\u0160t\u011bp\u00e1nek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning","year":"2008","unstructured":"Armando, A., Baumgartner, P., Dowek, G. (eds.): IJCAR 2008. LNCS (LNAI), vol.\u00a05195. Springer, Heidelberg (2008)"},{"key":"21_CR2","unstructured":"Carlson, A., Cumby, C., Rosen, J., Roth, D.: SNoW User\u2019s Guide. Technical Report UIUC-DCS-R-99-210, University of Illinois at Urbana-Champaign (1999)"},{"key":"21_CR3","unstructured":"Denzinger, J., Fuchs, M., Goller, C., Schulz, S.: Learning from Previous Proof Experience. Technical Report AR99-4, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (1999)"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: CADE 11 (2011) (To appear)","DOI":"10.1007\/978-3-642-22438-6_23"},{"issue":"1","key":"21_CR5","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. Autom. Reasoning\u00a040(1), 35\u201360 (2008)","journal-title":"J. Autom. Reasoning"},{"issue":"1-2","key":"21_CR6","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J. Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: leanCoP: Lean Connection-Based Theorem Proving. Journal of Symbolic Computation\u00a036(1-2), 139\u2013161 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Otten, J.: leanCoP 2.0 and ileanCoP 1.2: High performance lean theorem proving in classical and intuitionistic logic (system descriptions). In: Armando, A., et al. (eds.) [1], pp. 283\u2013291","DOI":"10.1007\/978-3-540-71070-7_23"},{"issue":"2-3","key":"21_CR8","doi-asserted-by":"crossref","first-page":"159","DOI":"10.3233\/AIC-2010-0464","volume":"23","author":"J. Otten","year":"2010","unstructured":"Otten, J.: Restricting backtracking in connection calculi. AI Commun.\u00a023(2-3), 159\u2013182 (2010)","journal-title":"AI Commun."},{"key":"21_CR9","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR 2006. CEUR, vol.\u00a0192, pp. 18\u201333 (2006)"},{"issue":"2-3","key":"21_CR10","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"issue":"2-3","key":"21_CR11","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E: A Brainiac Theorem Prover. AI Communications\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Communications"},{"key":"21_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809682","volume-title":"Kernel Methods for Pattern Analysis","author":"J. Shawe-Taylor","year":"2004","unstructured":"Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, Cambridge (2004)"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-642-04617-9_36","volume-title":"KI 2009: Advances in Artificial Intelligence","author":"M. Suda","year":"2009","unstructured":"Suda, M., Sutcliffe, G., Wischnewski, P., Lamotte-Schubert, M., de Melo, G.: External Sources of Axioms in Automated Theorem Proving. In: Mertsching, B., Hund, M., Aziz, Z. (eds.) KI 2009. LNCS, vol.\u00a05803, pp. 281\u2013288. Springer, Heidelberg (2009)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Tsivtsivadze, E., Urban, J., Geuvers, H., Heskes, T.: Semantic graph kernels for automated reasoning. In: SDM 2011 (to appear, 2011)","DOI":"10.1137\/1.9781611972818.68"},{"issue":"1","key":"21_CR15","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1142\/S0218213006002588","volume":"15","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. International Journal on Artificial Intelligence Tools\u00a015(1), 109\u2013130 (2006)","journal-title":"International Journal on Artificial Intelligence Tools"},{"issue":"1-2","key":"21_CR16","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning\u00a037(1-2), 21\u201343 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the Mizar Mathematical Library. In: ICMS, pp. 155\u2013166 (2010)","DOI":"10.1007\/978-3-642-15582-6_30"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vysko\u010dil, J.: MaLARea SG1- machine learner for automated reasoning with semantic guidance. In: Armando, et al. (eds.) [1], pp. 441\u2013456","DOI":"10.1007\/978-3-540-71070-7_37"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22119-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,20]],"date-time":"2020-06-20T04:55:56Z","timestamp":1592628956000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22119-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221187","9783642221194"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22119-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}