{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T06:56:18Z","timestamp":1761807378481},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_20","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"295-310","source":"Crossref","is-referenced-by-count":24,"title":["SRASS - A Semantic Relevance Axiom Selection System"],"prefix":"10.1007","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]},{"given":"Yury","family":"Puzis","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_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":"20_CR2","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, Miami, USA (2003)"},{"key":"20_CR3","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)"},{"key":"20_CR4","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-94-017-0437-3_11","volume-title":"Automated Deduction - A Basis for Applications","author":"B. Fischer","year":"1998","unstructured":"Fischer, B., Schumann, J., Snelting, G.: Deduction-Based Software Component Retrieval. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction - A Basis for Applications. Applied Logic Series, vol.\u00a03, pp. 265\u2013292. Kluwer, Dordrecht (1998)"},{"key":"20_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BFb0054243","volume-title":"Automated Deduction - CADE-15","author":"M. Fuchs","year":"1998","unstructured":"Fuchs, M.: System Description: Similarity-Based Lemma Generation for Model Elimination. In: Kirchner, C., Kirchner, H. (eds.) Automated Deduction - CADE-15. LNCS (LNAI), vol.\u00a01421, pp. 33\u201337. Springer, Heidelberg (1998)"},{"issue":"2","key":"20_CR6","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":"20_CR7","unstructured":"MacCartney, B., McIlraith, S., Amir, E., Uribe, T.: Practical Partition-Based Theorem Proving for Large Knowledge Bases. In: Gottlob G., Walsh, T. (eds.) Proceedings of the 18th International Joint Conference on Artificial Intelligence, pp. 89\u201396 (2003)"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"McCune, W.W.: Otter 3.0 Reference Manual and Guide. Technical Report ANL-94\/6, Argonne National Laboratory, Argonne, USA (1994)","DOI":"10.2172\/10129052"},{"key":"20_CR9","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\u201906 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning, CEUR Workshop Proceedings, vol. 192, pp. 53\u201369 (2006)"},{"key":"20_CR10","unstructured":"Meng, J., Paulson, L.: Translating Higher-Order Problems to First-Order Clauses. 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. 192, pp. 70\u201380 (2006)"},{"issue":"1-2","key":"20_CR11","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":"20_CR12","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. 192, pp. 34\u201352 (2006)"},{"key":"20_CR13","unstructured":"Pudlak, P.: Draft Thesis: Verification of Mathematical Proofs (2007)"},{"key":"20_CR14","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, Boston (1992)"},{"key":"20_CR15","unstructured":"Rabe, F.: Towards Determining the Subset Relation between Propositional Modal Logics. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) Proceedings of the FLoC\u201906 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning, CEUR Workshop Proceedings, vol. 192 (2006)"},{"key":"20_CR16","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)"},{"key":"20_CR17","first-page":"14","volume-title":"Proceedings of the 19th International FLAIRS Conference","author":"M. Sahami","year":"2006","unstructured":"Sahami, M.: Mining the Web to Determine Similarity Between Words, Objects, and Communities. In: Sutcliffe, G., Goebel, R. (eds.) Proceedings of the 19th International FLAIRS Conference, pp. 14\u201319. AAAI Press, Stanford (2006)"},{"issue":"2-3","key":"20_CR18","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":"20_CR19","unstructured":"Shen, W.: Automated Proofs of Equivalence of Modal Logic Systems. Master\u2019s thesis, Department of Computer Science, University of Miami, Miami, USA (2006)"},{"key":"20_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11814771_5","volume-title":"Automated Reasoning","author":"V. Sorge","year":"2006","unstructured":"Sorge, V., Meier, A., McCasland, R., Colton, S.: Automatic Construction and Verification of Isotopy Invariants. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 36\u201351. Springer, Heidelberg (2006)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/10721959_31","volume-title":"Automated Deduction - CADE-17","author":"G. Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: SystemOnTPTP. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol.\u00a01831, pp. 406\u2013410. Springer, Heidelberg (2000)"},{"key":"20_CR22","unstructured":"Sutcliffe, G.: The 3rd IJCAR Automated Theorem Proving Competition. AI Communications (to appear)"},{"key":"20_CR23","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, Stanford (2003)"},{"key":"20_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/11814771_7","volume-title":"Automated Reasoning","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Van Gelder, A.: Using the TPTP Language for Writing Derivations and Finite Interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 67\u201381. Springer, Heidelberg (2006)"},{"issue":"2","key":"20_CR25","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":"20_CR26","series-title":"Frontiers in Artificial Intelligence and Applications, no. 112","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, no. 112, pp. 201\u2013215. IOS Press, Amsterdam (2004)"},{"issue":"4","key":"20_CR27","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":"20_CR28","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10817-006-9032-3","volume":"37","author":"J. Urban","year":"2007","unstructured":"Urban, J.: MPTP 0.2: Design, Implementation, and Initial Experiments. Journal of Automated Reasoning\u00a037(1-2), 21\u201343 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"20_CR29","unstructured":"Urban, J., Sutcliffe, G.: The MPTP $100 Challenges (2006), http:\/\/www.tptp.org\/MPTPChallenge\/"},{"issue":"3","key":"20_CR30","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":"20_CR31","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-45620-1_22","volume-title":"Automated Deduction - CADE-18","author":"C. Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS Version 2.0. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol.\u00a02392, pp. 275\u2013279. Springer, Heidelberg (2002)"},{"key":"20_CR32","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)"},{"key":"20_CR33","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11814771_12","volume-title":"Automated Reasoning","author":"J. Zimmer","year":"2006","unstructured":"Zimmer, J., Autexier, S.: The MathServe System for Semantic Web Reasoning Services. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 17\u201320. Springer, Heidelberg (2006)"},{"key":"20_CR34","unstructured":"Zimmer, J., Meier, A., Sutcliffe, G., Zhang, Y.: Integrated Proof Transformation Services. In: Benzm\u00fcller, C., Windsteiger, W. (eds.) Proceedings of the Workshop on Computer-Supported Mathematical Theory Development, 2nd International Joint Conference on Automated Reasoning, Electronic Notes in Theoretical Computer Science (2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:03Z","timestamp":1619517183000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}