{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,23]],"date-time":"2026-09-23T10:34:19Z","timestamp":1790159659745,"version":"4.1.0"},"reference-count":66,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,9,22]],"date-time":"2015-09-22T00:00:00Z","timestamp":1442880000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council (GB)","doi-asserted-by":"publisher","award":["EP\/D070511\/1"],"award-info":[{"award-number":["EP\/D070511\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft (DE)","doi-asserted-by":"publisher","award":["BE 2501\/6-1"],"award-info":[{"award-number":["BE 2501\/6-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft (DE)","doi-asserted-by":"publisher","award":["BE 2501\/8-1"],"award-info":[{"award-number":["BE 2501\/8-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft (DE)","doi-asserted-by":"publisher","award":["BE 2501\/9-1"],"award-info":[{"award-number":["BE 2501\/9-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,12]]},"DOI":"10.1007\/s10817-015-9348-y","type":"journal-article","created":{"date-parts":[[2015,9,22]],"date-time":"2015-09-22T06:26:12Z","timestamp":1442903172000},"page":"389-404","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":39,"title":["The Higher-Order Prover Leo-II"],"prefix":"10.1007","volume":"55","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nik","family":"Sultana","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frank","family":"Thei\u00df","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,9,22]]},"reference":[{"issue":"4","key":"9348_CR1","doi-asserted-by":"crossref","first-page":"80","DOI":"10.4018\/jswis.2012100105","volume":"8","author":"J \u00c1lvez","year":"2012","unstructured":"\u00c1lvez, J., Lucio, P., Rigau, G.: Adimen-SUMO: reengineering an ontology for first-order reasoning. Int. J. Semantic Web Inf. Syst. 8(4), 80\u2013116 (2012)","journal-title":"Int. J. Semantic Web Inf. Syst."},{"issue":"3","key":"9348_CR2","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/BF00248320","volume":"5","author":"PB Andrews","year":"1989","unstructured":"Andrews, P.B.: On connections and higher order logic. J. Autom. Reason. 5(3), 257\u2013291 (1989)","journal-title":"J. Autom. Reason."},{"key":"9348_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9934-4","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Applied Logic Series","author":"PB Andrews","year":"2002","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Applied Logic Series, vol. 27. Springer, Berlin (2002)"},{"issue":"3","key":"9348_CR4","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"PB Andrews","year":"1996","unstructured":"Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: a theorem-proving system for classical type theory. J. Autom. Reason. 16(3), 321\u2013353 (1996)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9348_CR5","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/s10817-011-9233-2","volume":"47","author":"J Backes","year":"2011","unstructured":"Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. J. Autom. Reason. 47(4), 451\u2013479 (2011)","journal-title":"J. Autom. Reason."},{"key":"9348_CR6","unstructured":"Benzm\u00fcller, C.: A calculus and a system architecture for extensional higher-order resolution. Research Report 97-198, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, USA (1997)"},{"key":"9348_CR7","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C.: Extensional higher-order paramodulation and RUE-resolution. In: Ganzinger, H. (ed.) Automated Deduction\u2014CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7\u201310, 1999, Proceedings, no. 1632 in LNCS, pp. 399\u2013413. Springer (1999). doi: 10.1007\/3-540-48660-7_39","DOI":"10.1007\/3-540-48660-7_39"},{"issue":"1\u20132","key":"9348_CR8","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1023\/A:1020840027781","volume":"133","author":"C Benzm\u00fcller","year":"2002","unstructured":"Benzm\u00fcller, C.: Comparing approaches to resolution based higher-order theorem proving. Synthese 133(1\u20132), 203\u2013235 (2002). doi: 10.1023\/A:1020840027781","journal-title":"Synthese"},{"key":"9348_CR9","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C.: Automating access control logic in simple type theory with LEO-II. In: Gritzalis, D., L\u00f3pez, J. (eds.) Emerging Challenges for Security, Privacy and Trust, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18\u201320, 2009. Proceedings, IFIP, vol. 297, pp. 387\u2013398. Springer (2009). doi: 10.1007\/978-3-642-01244-0_34","DOI":"10.1007\/978-3-642-01244-0_34"},{"issue":"1\u20132","key":"9348_CR10","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s10472-011-9249-7","volume":"62","author":"C Benzm\u00fcller","year":"2011","unstructured":"Benzm\u00fcller, C.: Combining and automating classical and non-classical logics in classical higher-order logic. Ann. Math. Artif. Intell. (CLIMA XI) 62(1\u20132), 103\u2013128 (2011). doi: 10.1007\/s10472-011-9249-7","journal-title":"Ann. Math. Artif. Intell. (CLIMA XI)"},{"key":"9348_CR11","unstructured":"Benzm\u00fcller, C.: Automating quantified conditional logics in HOL. In: Rossi, F. (ed.) 23rd International Joint Conference on Artificial Intelligence (IJCAI-13), pp. 746\u2013753. Beijing, China (2013a)"},{"key":"9348_CR12","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C.: A top-down approach to combining logics. In: Proceedings of the 5th International Conference on Agents and Artificial Intelligence (ICAART), pp. 346\u2013351. SciTePress Digital Library, Barcelona (2013b). doi: 10.5220\/0004324803460351","DOI":"10.5220\/0004324803460351"},{"key":"9348_CR13","first-page":"171","volume-title":"All about Proofs, Proof for All, Mathematical Logic and Foundations","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C.: Higher-order automated theorem provers. In: Delahaye, D., Woltzenlogel\u00a0Paleo, B. (eds.) All about Proofs, Proof for All, Mathematical Logic and Foundations, pp. 171\u2013214. College Publications, London (2015)"},{"key":"9348_CR14","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Brown, C.: A structured set of higher-order problems. In: Hurd, J., Melham, T.F. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22\u201325, 2005, Proceedings, Springer, no. 3603 in LNCS, pp. 66\u201381 (2005). doi: 10.1007\/11541868_5","DOI":"10.1007\/11541868_5"},{"key":"9348_CR15","unstructured":"Benzm\u00fcller, C., Brown, C.: The curious inference of Boolos in MIZAR and OMEGA. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof - Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10(23), pp. 299\u2013388. The University of Bialystok, Polen (2007)"},{"key":"9348_CR16","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Kohlhase, M.: LEO\u2014a higher-order theorem prover. In: Kirchner, C., Kirchner, H. (eds), Automated Deduction\u2014CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5\u201310, 1998, Proceedings, Springer, no. 1421 in LNCS, pp. 139\u2013143 (1998). doi: 10.1007\/BFb0054256","DOI":"10.1007\/BFb0054256"},{"issue":"6","key":"9348_CR17","doi-asserted-by":"crossref","first-page":"881","DOI":"10.1093\/jigpal\/jzp080","volume":"18","author":"C Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C., Paulson, L.: Multimodal and intuitionistic logics in simple type theory. Logic J. IGPL 18(6), 881\u2013892 (2010). doi: 10.1093\/jigpal\/jzp080","journal-title":"Logic J. IGPL"},{"issue":"1","key":"9348_CR18","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logica Universalis 7(1), 7\u201320 (2013). doi: 10.1007\/s11787-012-0052-y","journal-title":"Logica Universalis"},{"key":"9348_CR19","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Sultana, N.: LEO-II version 1.5. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013, EasyChair, EPiC Series, vol.\u00a014, pp. 2\u201310 (2013)","DOI":"10.29007\/lbxw"},{"key":"9348_CR20","unstructured":"Benzm\u00fcller, C., Sultana, N.: Update report: LEO-II version 1.5. CoRR abs\/1303.3761 (2013)"},{"key":"9348_CR21","unstructured":"Benzm\u00fcller, C., Woltzenlogel\u00a0Paleo, B.: Formalization, mechanization and automation of G\u00f6del\u2019s proof of God\u2019s existence (2013). arXiv:1308.4526"},{"key":"9348_CR22","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Woltzenlogel\u00a0Paleo, B.: Automating G\u00f6del\u2019s ontological proof of God\u2019s existence with higher-order automated theorem provers. In: Schaub, T., Friedrich, G., O\u2019Sullivan, B. (eds.) ECAI 2014, IOS Press, Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93\u201398 (2014). doi: 10.3233\/978-1-61499-419-0-93","DOI":"10.3233\/978-1-61499-419-0-93"},{"key":"9348_CR23","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Woltzenlogel\u00a0Paleo, B.: Higher-order modal logics: Automation and applications. In: Paschke, A., Faber, W. (eds.) Reasoning Web 2015, no. 9203 in LNCS, pp. 1\u201343. Springer, Berlin (2015). doi: 10.1007\/978-3-319-21768-0_2","DOI":"10.1007\/978-3-319-21768-0_2"},{"key":"9348_CR24","unstructured":"Benzm\u00fcller, C., Ziener, M.: Automated consistency checking of expressive ontologies\u2014beware of the wrong interpretation of success!. In: Fink, M., Homola, M., Mileo, A., Varzinczak, I.J. (eds.) The 5th International Workshop on Acquisition, Representation and Reasoning with Contextualized Knowledge (ARCOE-LogIC 2013). Corunna, Spain (2013)"},{"issue":"4","key":"9348_CR25","doi-asserted-by":"crossref","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","volume":"69","author":"C Benzm\u00fcller","year":"2004","unstructured":"Benzm\u00fcller, C., Brown, C., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Log. 69(4), 1027\u20131088 (2004). doi: 10.2178\/jsl\/1102022211","journal-title":"J. Symb. Log."},{"issue":"3","key":"9348_CR26","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1016\/j.jal.2007.06.003","volume":"6","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined reasoning by automated cooperation. J. Appl. Log. 6(3), 318\u2013342 (2008). doi: 10.1016\/j.jal.2007.06.003","journal-title":"J. Appl. Log."},{"issue":"1:6","key":"9348_CR27","first-page":"1","volume":"5","author":"C Benzm\u00fcller","year":"2009","unstructured":"Benzm\u00fcller, C., Brown, C., Kohlhase, M.: Cut-simulation and impredicativity. Log. Methods Comput. Sci. 5(1:6), 1\u201321 (2009). doi: 10.2168\/LMCS-5(1:6)2009","journal-title":"Log. Methods Comput. Sci."},{"key":"9348_CR28","first-page":"53","volume-title":"Handbook of the 1st World Congress on Logic and Religion","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-H\u00e1jek ontological controversy. In: Silvestre, R.S., B\u00e9ziau, J.Y. (eds.) Handbook of the 1st World Congress on Logic and Religion, pp. 53\u201354. Joao Pessoa, Brasil (2015)"},{"key":"9348_CR29","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) Proceedings of TACAS 2013, LNCS, vol. 7795, pp. 493\u2013507. Springer (2013). doi: 10.1007\/978-3-642-36742-7_34","DOI":"10.1007\/978-3-642-36742-7_34"},{"key":"9348_CR30","doi-asserted-by":"crossref","unstructured":"Brown, C.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning (IJCAR 2012), LNCS, vol. 7364, pp. 111\u2013117. Springer, Berlin (2012). doi: 10.1007\/978-3-642-31365-3_11","DOI":"10.1007\/978-3-642-31365-3_11"},{"issue":"5","key":"9348_CR31","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N Bruijn de","year":"1972","unstructured":"de Bruijn, N.: Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math. 34(5), 381\u2013392 (1972)","journal-title":"Indag. Math."},{"key":"9348_CR32","doi-asserted-by":"crossref","unstructured":"Claessen, K., Lilliestr\u00f6m, A., Smallbone, N.: Sort it out with monotonicity. In: Proceedings of CADE-23, LNAI, vol. 6803, pp. 207\u2013221. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_17"},{"issue":"2","key":"9348_CR33","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/5383.5389","volume":"33","author":"VJ Digricoli","year":"1986","unstructured":"Digricoli, V.J., Harrison, M.C.: Equality-based binary resolution. J ACM 33(2), 253\u2013289 (1986). doi: 10.1145\/5383.5389","journal-title":"J ACM"},{"key":"9348_CR34","volume-title":"Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic","author":"M Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"9348_CR35","doi-asserted-by":"crossref","unstructured":"Hales, T: Mathematics in the Age of the Turing Machine. ArXiv e-prints arXiv:1302.2898 (2013)","DOI":"10.1017\/CBO9781107338579.008"},{"key":"9348_CR36","doi-asserted-by":"crossref","unstructured":"Harrison, J.: HOL Light: An overview. In: Proceedings of TPHOLs 2009, LNCS, vol. 5674, pp. 60\u201366. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"9348_CR37","unstructured":"Huet, G.: A complete mechanization of type theory. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence , pp. 139\u2013146 (1973a)"},{"issue":"1","key":"9348_CR38","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed lambda-calculus. Theor. Comput. Sci. 1(1), 27\u201357 (1975)","journal-title":"Theor. Comput. Sci."},{"key":"9348_CR39","unstructured":"Huet, G.P.: Constrained resolution: a complete method for higher order logic. Ph.D. thesis, Case Western Reserve University (1972)"},{"key":"9348_CR40","unstructured":"Huet, G.P.: A mechanization of type theory. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, pp. 139\u2013146 (1973b)"},{"issue":"2","key":"9348_CR41","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014). doi: 10.1007\/s10817-014-9303-3","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9348_CR42","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination-tree indexing and path indexing for term retrieval. J. Autom. Reason. 9(2), 147\u2013167 (1992)","journal-title":"J. Autom. Reason."},{"key":"9348_CR43","unstructured":"Miller, D.: Proofs in higher-order logic. Ph.D. thesis, Carnegie Mellon University (1983)"},{"issue":"2","key":"9348_CR44","doi-asserted-by":"crossref","first-page":"479","DOI":"10.2307\/2586480","volume":"64","author":"G Mints","year":"1999","unstructured":"Mints, G.: Cut-elimination for simple type theory with an axiom of choice. J. Symb. Log. 64(2), 479\u2013485 (1999)","journal-title":"J. Symb. Log."},{"key":"9348_CR45","doi-asserted-by":"crossref","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The heterogeneous tool set, Hets. In: Proceedings of TACAS 2007, LNCS, vol. 4424, pp. 519\u2013522. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_40"},{"key":"9348_CR46","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: Proceedings of IJCAR-01, LNAI, vol. 2083, pp. 257\u2013271. Springer (2001)","DOI":"10.1007\/3-540-45744-5_19"},{"key":"9348_CR47","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. No. 2283 in LNCS. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"1","key":"9348_CR48","doi-asserted-by":"crossref","first-page":"79","DOI":"10.3233\/AIC-120549","volume":"26","author":"A Pease","year":"2013","unstructured":"Pease, A., Benzm\u00fcller, C.: Sigma: an integrated development environment for formal ontology. AI Commun. 26(1), 79\u201397 (2013). doi: 10.3233\/AIC-120549","journal-title":"AI Commun."},{"key":"9348_CR49","unstructured":"Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, no. 257 in CEUR Workshop Proceedings, pp. 59\u201369 (2007)"},{"key":"9348_CR50","doi-asserted-by":"crossref","unstructured":"Pientka, B.: Higher-order substitution tree indexing. In: Palamidessi, C. (ed.) Proceedings of ICLP 2003, LNCS, vol. 2916, pp. 377\u2013391. Springer (2003)","DOI":"10.1007\/978-3-540-24599-5_26"},{"issue":"2","key":"9348_CR51","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"2","key":"9348_CR52","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - A brainiac theorem prover. AI Commun. 15(2), 111\u2013126 (2002)","journal-title":"AI Commun."},{"issue":"4","key":"9348_CR53","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1016\/j.jal.2005.10.008","volume":"4","author":"J Siekmann","year":"2006","unstructured":"Siekmann, J., Benzm\u00fcller, C., Autexier, S.: Computer supported mathematics with OMEGA. J. Appl. Log. 4(4), 533\u2013559 (2006). doi: 10.1016\/j.jal.2005.10.008","journal-title":"J. Appl. Log."},{"key":"9348_CR54","doi-asserted-by":"crossref","unstructured":"Sobel, J.: Logic and Theism: Arguments for and Against Beliefs in God, Cambridge U. Press, chap Appendix B. Notes in Dana Scott\u2019s Hand, pp. 145\u2013146 (2004a)","DOI":"10.1017\/CBO9780511497988"},{"key":"9348_CR55","doi-asserted-by":"crossref","unstructured":"Sobel, J.: Logic and Theism: Arguments for and Against Beliefs in God, Cambridge U. Press, chap Appendix A. Notes in Kurt G\u00f6del\u2019s Hand, pp. 144\u2013145 (2004b)","DOI":"10.1017\/CBO9780511497988"},{"key":"9348_CR56","doi-asserted-by":"crossref","unstructured":"Stalnaker, R.: A theory of conditionals. In: Studies in Logical Theory, Oxford, pp. 98\u2013112 (1968)","DOI":"10.1007\/978-94-009-9117-0_2"},{"key":"9348_CR57","doi-asserted-by":"crossref","unstructured":"Stickel, M.: The path-indexing method for indexing terms. Tech. Rep. 473, Artificial Intelligence Center, SRI International, 333 Ravenswood Ave., Menlo Park, CA 94025 (1989)","DOI":"10.21236\/ADA460990"},{"key":"9348_CR58","unstructured":"Sultana, N.: Higher-order proof translation. Ph.D. thesis, Computer Laboratory, University of Cambridge, Available as Tech Report UCAM-CL-TR-867 (2015)"},{"key":"9348_CR59","doi-asserted-by":"crossref","unstructured":"Sultana, N., Benzm\u00fcller, C.: Understanding LEO-II\u2019s proofs. In: Korovin, K., Schulz, S., Ternovska, E. (eds.) IWIL 2012, EasyChair, Merida, Venezuela, EPiC Series, vol.\u00a022, pp. 33\u201352 (2013)","DOI":"10.29007\/x9c9"},{"key":"9348_CR60","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M., Voronkov, A. (eds.) Proceedings of the 2nd International Computer Science Symposium in Russia, pp. 7\u201323. Springer, LNCS (2007)","DOI":"10.1007\/978-3-540-74510-5_4"},{"key":"9348_CR61","unstructured":"Sutcliffe, G.: The SZS ontologies for automated reasoning software. In: LPAR Workshops, CEUR Workshop Proceedings ( http:\/\/ceur-ws.org\/ ), vol. 418 (2008)"},{"issue":"4","key":"9348_CR62","doi-asserted-by":"crossref","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. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"key":"9348_CR63","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP World\u2014Infrastructure for Automated Reasoning. In: Proceedings of LPAR-16, no. 6355 in LNAI, pp. 1\u201312. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_1"},{"issue":"1","key":"9348_CR64","first-page":"1","volume":"3","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1\u201327 (2010)","journal-title":"J. Formaliz. Reason."},{"key":"9348_CR65","unstructured":"Thei\u00df, F., Benzm\u00fcller, C.: Term indexing for the LEO-II prover. In: IWIL-6 workshop at LPAR, : The 6th International Workshop on the Implementation of Logics. Pnom Penh, Cambodia (2006)"},{"key":"9348_CR66","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: Spass version 2.0. In: Voronkov, A. (ed) Proceedings of CADE 2002, LNCS, vol. 2392, pp. 275\u2013279. Springer (2002)","DOI":"10.1007\/3-540-45620-1_22"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9348-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9348-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9348-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T19:00:54Z","timestamp":1748631654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9348-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,22]]},"references-count":66,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,12]]}},"alternative-id":["9348"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9348-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,22]]}}}