{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T12:04:32Z","timestamp":1757592272743,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030582845"},{"type":"electronic","value":"9783030582852"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-58285-2_9","type":"book-chapter","created":{"date-parts":[[2020,9,10]],"date-time":"2020-09-10T09:00:01Z","timestamp":1599728401000},"page":"116-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding"],"prefix":"10.1007","author":[{"given":"Irina","family":"Makarenko","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,9,9]]},"reference":[{"issue":"2","key":"9_CR1","doi-asserted-by":"publisher","first-page":"395","DOI":"10.2307\/2272982","volume":"37","author":"PB Andrews","year":"1972","unstructured":"Andrews, P.B.: General models and extensionality. J. Symbol. Logic 37(2), 395\u2013397 (1972)","journal-title":"J. Symbol. Logic"},{"issue":"2","key":"9_CR2","doi-asserted-by":"publisher","first-page":"385","DOI":"10.2307\/2272981","volume":"37","author":"PB Andrews","year":"1972","unstructured":"Andrews, P.B.: General models, descriptions, and choice in type theory. J. Symbol. Logic 37(2), 385\u2013394 (1972)","journal-title":"J. Symbol. Logic"},{"issue":"4\u20135","key":"9_CR3","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1080\/00455091.2016.1201387","volume":"46","author":"A Bacon","year":"2016","unstructured":"Bacon, A., Hawthorne, J., Uzquiano, G.: Higher-order free logic and the Prior-Kaplan paradox. Canadian J. Philos. 46(4\u20135), 493\u2013541 (2016)","journal-title":"Canadian J. Philos."},{"key":"9_CR4","series-title":"Volume III: Alternatives in Classical Logic","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-94-009-5203-4_6","volume-title":"Handbook of Philosophical Logic","author":"E Bencivenga","year":"1986","unstructured":"Bencivenga, E.: Free logics. In: Gabbay, D.M., G\u00fcnthner, F. (eds.) Handbook of Philosophical Logic. Volume III: Alternatives in Classical Logic, pp. 373\u2013426. Springer, Netherlands, Dordrecht (1986)"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1016\/j.scico.2018.10.008","volume":"172","author":"C Benzm\u00fcller","year":"2019","unstructured":"Benzm\u00fcller, C.: Universal (Meta-)logical reasoning: recent successes. Sci. Comput. Program. 172, 48\u201362 (2019)","journal-title":"Sci. Comput. Program."},{"key":"9_CR6","unstructured":"Benzm\u00fcller, C., Andrews, P.B.: Church\u2019s type theory. In: Zalta, E.N. (ed.), The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, summer 2019 edition (2019)"},{"issue":"4","key":"9_CR7","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.E., Kohlhase, M.: Higher-order semantics and extensionality. J. Symbol. Logic 69(4), 1027\u20131088 (2004)","journal-title":"J. Symbol. Logic"},{"key":"9_CR8","series-title":"Handbook of the History of Logic","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/B978-0-444-51624-4.50005-8","volume-title":"Computational Logic","author":"C Benzm\u00fcller","year":"2014","unstructured":"Benzm\u00fcller, C., Miller, D.: Automation of higher-order logic. In: Gabbay, D.M., Siekmann, J.H., Woods, J. (eds.) Computational Logic. Handbook of the History of Logic, vol. 9, pp. 215\u2013254. Elsevier, North Holland (2014)"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"103348","DOI":"10.1016\/j.artint.2020.103348","volume":"287","author":"C Benzm\u00fcller","year":"2020","unstructured":"Benzm\u00fcller, C., Parent, X., van der Torre, L.: Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. Artif. Intell. 287, 103348 (2020)","journal-title":"Artif. Intell."},{"issue":"1","key":"9_CR10","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10817-018-09507-7","volume":"64","author":"C Benzm\u00fcller","year":"2019","unstructured":"Benzm\u00fcller, C., Scott, D.S.: Automating free logic in HOL, with an experimental application in category theory. J. Autom. Reason. 64(1), 53\u201372 (2019). \n                    https:\/\/doi.org\/10.1007\/s10817-018-09507-7","journal-title":"J. Autom. Reason."},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-14052-5_11","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2010","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.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"CE Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012). \n                    https:\/\/doi.org\/10.1007\/978-3-642-31365-3_11"},{"issue":"2","key":"9_CR13","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. Symbol. Logic 5(2), 56\u201368 (1940)","journal-title":"J. Symbol. Logic"},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"1269","DOI":"10.2307\/2274487","volume":"55","author":"WM Farmer","year":"1990","unstructured":"Farmer, W.M.: A Partial Functions Version of Church\u2019s Simple Theory of Types. J. Symbol. Log. 55, 1269\u20131291 (1990)","journal-title":"J. Symbol. Log."},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-1-4612-2822-6_5","volume-title":"Logic from Computer Science","author":"S Feferman","year":"1992","unstructured":"Feferman, S.: Logics for termination and correctness of functional programs. In: Moschovakis, Y.N. (ed.) Logic from Computer Science, pp. 95\u2013127. Springer, New York (1992). \n                    https:\/\/doi.org\/10.1007\/978-1-4612-2822-6_5"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-94-015-9761-6_9","volume-title":"New Essays in Free Logic. In Honour of Karel Lambert","author":"RD Gumb","year":"2001","unstructured":"Gumb, R.D.: Free logic in program specification and verification. In: Morscher, E., Hieke, A. (eds.) New Essays in Free Logic. In Honour of Karel Lambert, vol. 23, pp. 157\u2013193. In Honour of Karel Lambert. Springer, Dordrecht (2001). \n                    https:\/\/doi.org\/10.1007\/978-94-015-9761-6_9"},{"issue":"1","key":"9_CR17","first-page":"25","volume":"7","author":"RD Gumb","year":"1997","unstructured":"Gumb, R.D., Lambert, K.: Definitions in nonstrict positive free logic. Modern Logic 7(1), 25\u201355 (1997)","journal-title":"Modern Logic"},{"issue":"2","key":"9_CR18","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L Henkin","year":"1950","unstructured":"Henkin, L.: Completeness in the theory of types. J. Symbol. Logic 15(2), 81\u201391 (1950)","journal-title":"J. Symbol. Logic"},{"key":"9_CR19","unstructured":"Kaplan, D.: A problem in possible worlds semantics. In: Sinnott-Armstrong, W., Raffman, D., Asher, N. (eds.) Modality, Morality and Belief: Essays in Honor of Ruth Barcan Marcus, pp. 41\u201352. Cambridge University Press, Cambridge (1995)"},{"issue":"1","key":"9_CR20","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1017\/S1755020319000297","volume":"13","author":"D Kirchner","year":"2020","unstructured":"Kirchner, D., Benzm\u00fcller, C., Zalta, E.N.: Mechanizing principia Logico-Metaphysica in functional type theory. Rev. Symbol. Logic 13(1), 206\u2013218 (2020)","journal-title":"Rev. Symbol. Logic"},{"key":"9_CR21","unstructured":"Lambert, K.: The Definition of E! in Free Logic. The International Congress for Logic, Methodology and Philosophy of Science, Abstracts (1960)"},{"issue":"8","key":"9_CR22","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1305\/ndjfl\/1093956251","volume":"1\u20132","author":"K Lambert","year":"1967","unstructured":"Lambert, K.: Free logic and the concept of existence. Notre Dame J. Formal Logic 1\u20132(8), 133\u2013144 (1967)","journal-title":"Notre Dame J. Formal Logic"},{"key":"9_CR23","volume-title":"Philosophical Applications of Free Logic","author":"K Lambert","year":"1991","unstructured":"Lambert, K.: Philosophical Applications of Free Logic. Oxford University Press, Oxford (1991)"},{"key":"9_CR24","series-title":"In Honour of Karel Lambert","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-94-015-9761-6_8","volume-title":"New Essays in Free Logic","author":"S Lehmann","year":"2001","unstructured":"Lehmann, S.: \u2018No Input, No Output\u2019 Logic. In: Morscher, E., Hieke, A. (eds.) New Essays in Free Logic. In Honour of Karel Lambert, vol. 23, pp. 147\u2013155. Springer, Netherlands, Dordrecht (2001). \n                    https:\/\/doi.org\/10.1007\/978-94-015-9761-6_8"},{"key":"9_CR25","unstructured":"Makarenko, I.: Free Higher-Order Logic - Notion, Definition and Embedding in HOL. Master\u2019s thesis, Freie Universit\u00e4t Berlin (2020)"},{"issue":"1","key":"9_CR26","doi-asserted-by":"publisher","first-page":"8","DOI":"10.2307\/2270048","volume":"33","author":"RK Meyer","year":"1968","unstructured":"Meyer, R.K., Lambert, K.: Universally free logic and standard quantification theory. J. Symbol. Logic 33(1), 8\u201326 (1968)","journal-title":"J. Symbol. Logic"},{"key":"9_CR27","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic (2019). \n                    http:\/\/isabelle.in.tum.de\/doc\/tutorial.pdf\n                    \n                  . Accessed 30 Dec 2019"},{"key":"9_CR28","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In: Proceedings of the 8th International Workshop on the Implementation of Logics, pp. 131\u2013146 (2015)"},{"issue":"1","key":"9_CR29","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1305\/ndjfl\/1093956750","volume":"2","author":"AN Prior","year":"1961","unstructured":"Prior, A.N.: On a Family of Paradoxes. Notre Dame J. Formal Logic 2(1), 16\u201332 (1961)","journal-title":"Notre Dame J. Formal Logic"},{"key":"9_CR30","volume-title":"Logics Without Existence Assumptions","author":"R Schock","year":"1968","unstructured":"Schock, R.: Logics Without Existence Assumptions. Almqvist & Wiksell, Stockholm (1968)"},{"issue":"4","key":"9_CR31","doi-asserted-by":"publisher","first-page":"305","DOI":"10.2307\/2963525","volume":"25","author":"K Sch\u00fctte","year":"1960","unstructured":"Sch\u00fctte, K.: Syntactical and semantical properties of simple type theory. J. Symbol. Logic 25(4), 305\u2013326 (1960)","journal-title":"J. Symbol. Logic"},{"key":"9_CR32","unstructured":"Dana Scott. Existence and Description in Formal Logic. In Ralph Schoenman, editor, Bertrand Russell: Philosopher of the Century, pages 181\u2013200. Little, Brown & Company, Boston, 1967. Repr. in [23], pp. 28\u201348"},{"issue":"4","key":"9_CR33","first-page":"535","volume":"25","author":"A Steen","year":"2016","unstructured":"Steen, A., Benzm\u00fcller, C.: Sweet SIXTEEN: automation via embedding into classical higher-Order Logic. Logic Logical Philos. 25(4), 535\u2013554 (2016)","journal-title":"Logic Logical Philos."},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-94205-6_8","volume-title":"Automated Reasoning","author":"A Steen","year":"2018","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 108\u2013116. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-94205-6_8"},{"key":"9_CR35","unstructured":"Villadsen, J., Schlichtkrull, A.: Formalization of many-valued logics. In: Christiansen, H., Dolores Jim\u00e9nez-L\u00f3pez, M., Loukanova, R., Moss, L.S. (eds.), Partiality and Underspecification in Information, Languages, and Knowledge, pp. 219\u2013256. Cambridge Scholars Press (2017)"},{"key":"9_CR36","unstructured":"Zalta, E.N.: Principia Logico-Metaphysica. \n                    http:\/\/mally.stanford.edu\/principia.pdf\n                    \n                  . Draft\/Excerpt; Accessed 31 May 2020"}],"container-title":["Lecture Notes in Computer Science","KI 2020: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58285-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,10]],"date-time":"2020-09-10T15:15:34Z","timestamp":1599750934000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-58285-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030582845","9783030582852"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58285-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"9 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"KI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"German Conference on Artificial Intelligence (K\u00fcnstliche Intelligenz)","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bamberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"43","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ki2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ki2020.uni-bamberg.de\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"62","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Due to the Corona pandemic KI 2020 was held as a virtual event.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}