{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,26]],"date-time":"2025-12-26T14:26:39Z","timestamp":1766759199307,"version":"3.37.3"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["BE 2501\/9-2"],"award-info":[{"award-number":["BE 2501\/9-2"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001663","name":"Volkswagen Foundation","doi-asserted-by":"publisher","award":["CRAP"],"award-info":[{"award-number":["CRAP"]}],"id":[{"id":"10.13039\/501100001663","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":[[2020,1]]},"DOI":"10.1007\/s10817-018-09507-7","type":"journal-article","created":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T06:15:03Z","timestamp":1546323303000},"page":"53-72","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Automating Free Logic in HOL, with an Experimental Application in Category Theory"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3392-3093","authenticated-orcid":false,"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Dana S.","family":"Scott","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,1,1]]},"reference":[{"issue":"2","key":"9507_CR1","doi-asserted-by":"publisher","first-page":"395","DOI":"10.2307\/2272982","volume":"37","author":"P Andrews","year":"1972","unstructured":"Andrews, P.: General models and extensionality. J. Symb. Log. 37(2), 395\u2013397 (1972)","journal-title":"J. Symb. Log."},{"key":"9507_CR2","unstructured":"Andrews, P.: Church\u2019s type theory. In: Zalta, E. N (ed.) The Stanford Encyclopedia of Philosophy, Summer 2018 edn. Metaphysics Research Lab, Stanford University (2018). https:\/\/plato.stanford.edu\/archives\/sum2018\/entries\/type-theory-church\/"},{"key":"9507_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139032636","volume-title":"Lambda Calculus with Types. Perspectives in Logic","author":"H Barendregt","year":"2013","unstructured":"Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, Cambridge (2013)"},{"key":"9507_CR4","unstructured":"Benzm\u00fcller, C.: Automating quantified conditional logics in HOL. In: Rossi, F. (ed.) Proceedings of IJCAI-23. Beijing, China (2013)"},{"key":"9507_CR5","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s10992-016-9403-0","volume":"46","author":"C Benzm\u00fcller","year":"2016","unstructured":"Benzm\u00fcller, C.: Cut-elimination for quantified conditional logic. J. Philos. Log. 46, 333\u2013353 (2016)","journal-title":"J. Philos. Log."},{"issue":"4","key":"9507_CR6","doi-asserted-by":"publisher","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)","journal-title":"J. Symb. Log."},{"issue":"1:6","key":"9507_CR7","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)","journal-title":"Log. Methods Comput. Sci."},{"key":"9507_CR8","volume-title":"Handbook of the History of Logic, Volume 9\u2014Logic and Computation","author":"C Benzm\u00fcller","year":"2014","unstructured":"Benzm\u00fcller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J., Gabbay, D., Woods, J. (eds.) Handbook of the History of Logic, Volume 9\u2014Logic and Computation. Elsevier, Amsterdam (2014)"},{"key":"9507_CR9","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-42432-3_6","volume-title":"Mathematical Software \u2013 ICMS 2016","author":"Christoph Benzm\u00fcller","year":"2016","unstructured":"Benzm\u00fcller, C., Scott, D.: Automating free logic in Isabelle\/HOL. In: Greuel, G.M., Koch, T., Paule, P., Sommese, A. (eds.) Mathematical Software\u2014ICMS 2016, 5th International Congress, Proceedings, LNCS, vol. 9725, pp. 43\u201350. Springer, Berlin, Germany (2016)"},{"key":"9507_CR10","unstructured":"Benzm\u00fcller, C., Scott, D.S.: Axiomatizing category theory in free logic. CoRR (2016). arXiv:1609.01493"},{"key":"9507_CR11","unstructured":"Benzm\u00fcller, C., Scott, D.S.: Axiom systems for category theory in free logic. Archive of Formal Proofs (2018). https:\/\/www.isa-afp.org\/entries\/AxiomaticCategoryTheory.html"},{"key":"9507_CR12","unstructured":"Benzm\u00fcller, C., Steen, A., Wisniewski, M.: Leo-III version 1.1 (system description). In: Eiter, T., Sands, D. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)\u2014Short Papers, Kalpa Puplications. EasyChair, Maun, Botswana (2017) (to appear)"},{"issue":"4","key":"9507_CR13","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-015-9348-y","volume":"55","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Sultana, N., Paulson, L.C., Theiss, F.: The higher-order prover Leo-II. J. Autom. Reason. 55(4), 389\u2013404 (2015)","journal-title":"J. Autom. Reason."},{"key":"9507_CR14","unstructured":"Blanchette, J.C.: Hammering Away\u2014A Users Guide to Sledgehammer for Isabelle\/HOL. Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2018). https:\/\/isabelle.in.tum.de\/doc\/sledgehammer.pdf . With contributions from Lawrence C. Paulson"},{"issue":"1","key":"9507_CR15","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109\u2013128 (2013)","journal-title":"J. Autom. Reason."},{"key":"9507_CR16","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11\u201314, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6172, pp. 131\u2013146. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"9507_CR17","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle\u2014superposition with hard sorts and configurable simplification. In: Beringer, L., Felty, A.P. (eds.) Interactive Theorem Proving\u2014Third International Conference, ITP 2012, Princeton, NJ, USA, August 13\u201315, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7406, pp. 345\u2013360. Springer (2012)","DOI":"10.1007\/978-3-642-32347-8_24"},{"key":"9507_CR18","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning\u20146th International Joint Conference, IJCAR 2012, Manchester, UK, June 26\u201329, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7364, pp. 111\u2013117. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"9507_CR19","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"9507_CR20","unstructured":"Deters, M., Reynolds, A., King, T., Barrett, C.W., Tinelli, C.: A tour of CVC4: How it works, and how to use it. In: Claessen, K., Kuncak, V. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21\u201324, 2014, p.\u00a07. IEEE (2014)"},{"key":"9507_CR21","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9507_CR22","unstructured":"Freyd, P.: Amplifications, Diminutions, Subscorings for Categories, Allegories (2016). University of Pennsylvania. Unpublished. https:\/\/www.math.upenn.edu\/~pjf\/amplifications.pdf . Accessed Aug 2016"},{"key":"9507_CR23","volume-title":"Categories","author":"P Freyd","year":"1990","unstructured":"Freyd, P., Scedrov, A.: Categories. North Holland, Allegories (1990)"},{"key":"9507_CR24","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification\u201425th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp. 1\u201335. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9507_CR25","unstructured":"Lambert, K.: The definition of e(xistence)! in free logic. In: Abstracts: The International Congress for Logic, Methodology and Philosophy of Science. Stanford University Press, Stanford (1960)"},{"key":"9507_CR26","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139165068","volume-title":"Free Logic: Selected Essays","author":"K Lambert","year":"2002","unstructured":"Lambert, K.: Free Logic: Selected Essays. Cambridge University Press, Cambridge (2002)"},{"issue":"6","key":"9507_CR27","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1073\/pnas.34.6.263","volume":"34","author":"S MacLane","year":"1948","unstructured":"MacLane, S.: Groups, categories and duality. Proc. Nat. Acad. Sci. 34(6), 263\u2013267 (1948)","journal-title":"Proc. Nat. Acad. Sci."},{"key":"9507_CR28","unstructured":"Makarenko, I.: Automatisierung von Freier Logik in Logik H\u00f6herer Stufe. Bachelorarbeit. Freie Universit\u00e4t Berlin, Institut f\u00fcr Informatik (2016)"},{"key":"9507_CR29","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. No. 2283 in LNCS. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9507_CR30","unstructured":"Nolt, J.: Free logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Fall 2018 edn. Metaphysics Research Lab, Stanford University (2018). https:\/\/plato.stanford.edu\/archives\/fall2018\/entries\/logic-free\/"},{"key":"9507_CR31","doi-asserted-by":"crossref","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning\u201419th International Conference, LPAR-19, Stellenbosch, South Africa, December 14\u201319, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8312, pp. 735\u2013743. Springer (2013). http:\/\/dx.doi.org\/10.1007\/978-3-642-45221-5","DOI":"10.1007\/978-3-642-45221-5"},{"key":"9507_CR32","unstructured":"Scott, D.: Existence and description in formal logic. In: Schoenman, R. (ed.) Bertrand Russell: Philosopher of the Century, pp. 181\u2013200. George Allen & Unwin, London (1967) (Reprinted with additions in: Philosophical Application of Free Logic, edited by K. Lambert. Oxford Universitry Press, 1991, pp. 28\u201348)"},{"key":"9507_CR33","unstructured":"Scott, D.: Identity and existence in intuitionistic logic. In: Fourman, M., Mulvey, C., Scott, D. (eds.) Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9\u201321, 1977, Lecture Notes in Mathematics, vol. 752, pp. 660\u2013696. Springer, Berlin, Heidelberg (1979)"},{"issue":"1","key":"9507_CR34","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":"9507_CR35","unstructured":"Wisniewski, M., Steen, A., Benzm\u00fcller, C.: TPTP and beyond: representation of quantified non-classical logics. In: Benzm\u00fcller, C., Otten, J. (eds.) ARQNL 2016. Automated Reasoning in Quantified Non-Classical Logics, vol. 1770, pp. 51\u201365. CEUR Workshop Proceedings. http:\/\/ceur-ws.org (2016)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-09507-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-09507-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-09507-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,9]],"date-time":"2022-09-09T12:19:52Z","timestamp":1662725992000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-09507-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,1]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["9507"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-09507-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2019,1,1]]},"assertion":[{"value":"15 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 December 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 January 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}