{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T08:14:48Z","timestamp":1760170488308},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_37","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T05:56:30Z","timestamp":1219989390000},"page":"441-456","source":"Crossref","is-referenced-by-count":54,"title":["MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance"],"prefix":"10.1007","author":[{"given":"Josef","family":"Urban","sequence":"first","affiliation":[]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[]},{"given":"Petr","family":"Pudl\u00e1k","sequence":"additional","affiliation":[]},{"given":"Ji\u0159\u00ed","family":"Vysko\u010dil","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"37_CR1","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Darwin - A Theorem Prover for the Model Evolution Calculus. In: Sutcliffe, G., Schulz, S., Tammet, T. (eds.) Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning (2004)"},{"key":"37_CR2","unstructured":"Carlson, A., Cumby, C., Rosen, J., Roth, D.: SNoW User\u2019s Guide. Technical Report UIUC-DCS-R-99-210, University of Illinois, Urbana-Champaign (1999)"},{"key":"37_CR3","unstructured":"Claessen, K., Sorensson, N.: New Techniques that Improve MACE-style Finite Model Finding. In: Baumgartner, P., Fermueller, C. (eds.) Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)"},{"key":"37_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/978-3-540-25984-8_12","volume-title":"Automated Reasoning","author":"E. Denney","year":"2004","unstructured":"Denney, E., Fischer, B., Schumann, J.: Using Automated Theorem Provers to Certify Auto-generated Aerospace Software. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 198\u2013212. Springer, Heidelberg (2004)"},{"issue":"2","key":"37_CR5","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1006\/jsco.1999.0363","volume":"29","author":"M. Fuchs","year":"2000","unstructured":"Fuchs, M.: Controlled Use of Clausal Lemmas in Connection Tableau Calculi. Journal of Symbolic Computation\u00a029(2), 299\u2013341 (2000)","journal-title":"Journal of Symbolic Computation"},{"key":"37_CR6","doi-asserted-by":"crossref","unstructured":"McCune, W.W.: Mace4 Reference Manual and Guide. Technical Report ANL\/MCS-TM-264, Argonne National Laboratory, Argonne, USA (2003)","DOI":"10.2172\/822574"},{"key":"37_CR7","unstructured":"Meng, J., Paulson, L.: Lightweight Relevance Filtering for Machine-Generated Resolution Problems. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) Proceedings of the FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning. CEUR Workshop Proceedings, vol.\u00a0192, pp. 53\u201369 (2006)"},{"issue":"1","key":"37_CR8","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.: Translating Higher-order Problems to First-order Clauses. Journal of Automated Reasoning\u00a040(1), 35\u201360 (2008)","journal-title":"Journal of Automated Reasoning"},{"issue":"1-2","key":"37_CR9","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.: A Relevance Restriction Strategy for Automated Deduction. Artificial Intelligence\u00a0144(1-2), 59\u201393 (2003)","journal-title":"Artificial Intelligence"},{"key":"37_CR10","unstructured":"Pudlak, P.: Search for Faster and Shorter Proofs using Machine Generated lemmas. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) Proceedings of the FLoC 2006 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning. CEUR Workshop Proceedings, vol.\u00a0192, pp. 34\u201352 (2006)"},{"key":"37_CR11","unstructured":"Pudlak, P.: Draft Thesis: Verification of Mathematical Proofs (2007)"},{"key":"37_CR12","volume-title":"Automated Development of Fundamental Mathematical Theories","author":"A. Quaife","year":"1992","unstructured":"Quaife, A.: Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers, Dordrecht (1992)"},{"key":"37_CR13","unstructured":"Ramachandran, D., Reagan, P., Goolsbey, K.: First-orderized ResearchCyc: Expressiveness and Efficiency in a Common Sense Knowledge Base. In: Shvaiko, P. (ed.) Proceedings of the Workshop on Contexts and Ontologies: Theory, Practice and Applications (2005)"},{"issue":"2-3","key":"37_CR14","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":"37_CR15","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"},{"issue":"2","key":"37_CR16","first-page":"117","volume":"20","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G.: The 3rd IJCAR Automated Theorem Proving Competition. AI Communications\u00a020(2), 117\u2013126 (2007)","journal-title":"AI Communications"},{"key":"37_CR17","first-page":"108","volume-title":"Proceedings of the 16th International FLAIRS Conference","author":"G. Sutcliffe","year":"2003","unstructured":"Sutcliffe, G., Dvorsky, A.: Proving Harder Theorems by Axiom Reduction. In: Russell, I., Haller, S. (eds.) Proceedings of the 16th International FLAIRS Conference, pp. 108\u2013112. AAAI Press, Menlo Park (2003)"},{"key":"37_CR18","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":"2","key":"37_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.B.: 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":"37_CR20","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"201","volume-title":"Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems","author":"G. Sutcliffe","year":"2004","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP Data-Exchange Formats for Automated Theorem Proving Tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems. Frontiers in Artificial Intelligence and Applications, vol.\u00a0112, pp. 201\u2013215. IOS Press, Amsterdam (2004)"},{"issue":"4","key":"37_CR21","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1016\/j.jal.2005.10.004","volume":"4","author":"J. Urban","year":"2006","unstructured":"Urban, J.: MizarMode - An Integrated Proof Assistance Tool for the Mizar Way of Formalizing Mathematics. Journal of Applied Logic\u00a04(4), 414\u2013427 (2006)","journal-title":"Journal of Applied Logic"},{"issue":"1-2","key":"37_CR22","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. Journal of Automated Reasoning\u00a037(1-2), 21\u201343 (2006)","journal-title":"Journal of Automated Reasoning"},{"key":"37_CR23","unstructured":"Urban, J.: MaLARea: a Metasystem for Automated Reasoning in Large Theories. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, pp. 45\u201358 (2007)"},{"issue":"3","key":"37_CR24","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R. Veroff","year":"1996","unstructured":"Veroff, R.: Using Hints to Increase the Effectiveness of an Automated Reasoning Program: Case Studies. Journal of Automated Reasoning\u00a016(3), 223\u2013239 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"37_CR25","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining Superposition, Sorts and Splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965\u20132011. Elsevier Science, Amsterdam (2001)"},{"key":"37_CR26","unstructured":"Zhang, Y., Sutcliffe, G.: Lemma Management Techniques for Automated Theorem Proving. In: Konev, B., Schulz, S. (eds.) Proceedings of the 5th International Workshop on the Implementation of Logics, pp. 87\u201394 (2005)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:15:14Z","timestamp":1605744914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}