{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T07:01:14Z","timestamp":1761807674097,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642224379"},{"type":"electronic","value":"9783642224386"}],"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-22438-6_23","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T22:21:44Z","timestamp":1311027704000},"page":"299-314","source":"Crossref","is-referenced-by-count":63,"title":["Sine Qua Non for Large Theory Reasoning"],"prefix":"10.1007","author":[{"given":"Kry\u0161tof","family":"Hoder","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-02959-2_13","volume-title":"Automated Deduction \u2013 CADE-22","author":"A. Roederer","year":"2009","unstructured":"Roederer, A., Puzis, Y., Sutcliffe, G.: divvy: An ATP meta-system based on axiom relevance ordering. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 157\u2013162. Springer, Heidelberg (2009)"},{"key":"23_CR2","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":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-14203-1_16","volume-title":"Automated Reasoning","author":"K. Hoder","year":"2010","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination in vampire. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 188\u2013195. Springer, Heidelberg (2010)"},{"issue":"11","key":"23_CR4","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/219717.219745","volume":"38","author":"D.B. Lenat","year":"1995","unstructured":"Lenat, D.B.: CYC: A large-scale investment in knowledge infrastructure. Communications of the ACM\u00a038(11), 33\u201338 (1995)","journal-title":"Communications of the ACM"},{"issue":"1","key":"23_CR5","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":"23_CR6","doi-asserted-by":"crossref","unstructured":"Niles, I., Pease, A.: Towards a standard upper ontology. In: FOIS, pp. 2\u20139 (2001)","DOI":"10.1145\/505168.505170"},{"issue":"1-2","key":"23_CR7","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0004-3702(02)00368-5","volume":"144","author":"D.A. Plaisted","year":"2003","unstructured":"Plaisted, D.A., Yahya, A.H.: A relevance restriction strategy for automated deduction. Artif. Intell.\u00a0144(1-2), 59\u201393 (2003)","journal-title":"Artif. Intell."},{"key":"23_CR8","unstructured":"Pudlak, P.: Semantic selection of premisses for automated theorem proving. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.) ESARLT. CEUR Workshop Proceedings, vol.\u00a0257, pp. 27\u201344. (2007) CEUR-WS.org"},{"key":"23_CR9","first-page":"311","volume-title":"An overview of the mizar project","year":"1992","unstructured":"Rudnicki, P. (ed.): An overview of the mizar project, pp. 311\u2013332. University of Technology, Bastad (1992)"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: CASC-J4 the 4th IJCAR ATP system competition. In: Armando (ed.) [2], pp. 457\u2013458","DOI":"10.1007\/978-3-540-71070-7_38"},{"issue":"4","key":"23_CR11","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. J. Autom. Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"23_CR12","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/AIC-2010-0469","volume":"23","author":"G. Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The cade-22 automated theorem proving system competition - casc-22. AI Commun.\u00a023(1), 47\u201359 (2010)","journal-title":"AI Commun."},{"key":"23_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-73595-3_20","volume-title":"Automated Deduction \u2013 CADE-21","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G., Puzis, Y.: Srass - a semantic relevance axiom selection system. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 295\u2013310. Springer, Heidelberg (2007)"},{"issue":"1-2","key":"23_CR14","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":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-15582-6_30","volume-title":"Mathematical Software \u2013 ICMS 2010","author":"J. Urban","year":"2010","unstructured":"Urban, J., Hoder, K., Voronkov, A.: Evaluation of automated theorem proving on the mizar mathematical library. In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol.\u00a06327, pp. 155\u2013166. Springer, Heidelberg (2010)"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Urban, J., Sutcliffe, G., Pudl\u00e1k, P., Vyskocil, J.: Malarea sg1- machine learner for automated reasoning with semantic guidance. In: Armando (ed.) [2], pp. 441\u2013456.","DOI":"10.1007\/978-3-540-71070-7_37"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,21]],"date-time":"2020-06-21T11:45:01Z","timestamp":1592739901000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}