{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:07:44Z","timestamp":1784844464899,"version":"3.55.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,5,27]],"date-time":"2012-05-27T00:00:00Z","timestamp":1338076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Log. Univers."],"published-print":{"date-parts":[[2013,3]]},"DOI":"10.1007\/s11787-012-0052-y","type":"journal-article","created":{"date-parts":[[2012,5,26]],"date-time":"2012-05-26T03:50:58Z","timestamp":1338004258000},"page":"7-20","source":"Crossref","is-referenced-by-count":44,"title":["Quantified Multimodal Logics in Simple Type Theory"],"prefix":"10.1007","volume":"7","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2012,5,27]]},"reference":[{"key":"52_CR1","doi-asserted-by":"crossref","first-page":"395","DOI":"10.2307\/2272982","volume":"37","author":"P.B. Andrews","year":"1972","unstructured":"Andrews P.B.: General models and extensionality. J. Symb. Logic 37, 395\u2013397 (1972)","journal-title":"J. Symb. Logic"},{"key":"52_CR2","doi-asserted-by":"crossref","first-page":"385","DOI":"10.2307\/2272981","volume":"37","author":"P.B. Andrews","year":"1972","unstructured":"Andrews P.B.: General models, descriptions, and choice in type theory. J. Symb. Logic 37, 385\u2013394 (1972)","journal-title":"J. Symb. Logic"},{"key":"52_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","author":"P.B. Andrews","year":"2002","unstructured":"Andrews P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Kluwer, Dordrecht (2002)","edition":"2"},{"key":"52_CR4","unstructured":"Andrews, P.B.: Church\u2019s type theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Center for the Study of Language and Information, Stanford University (2009). http:\/\/plato.stanford.edu\/archives\/spr2009\/entries\/type-theory-church\/"},{"issue":"4","key":"52_CR5","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","volume":"4","author":"P.B. Andrews","year":"2006","unstructured":"Andrews P.B., Brown C.E.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Logic 4(4), 367\u2013395 (2006)","journal-title":"J. Appl. Logic"},{"key":"52_CR6","doi-asserted-by":"crossref","unstructured":"Armando, A., Baumgartner, P., Dowek, G. (eds.): Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12\u201315. Proceedings, LNCS, vol. 5195. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-71070-7"},{"key":"52_CR7","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. Proceedings, IFIP, vol. 297, pp. 387\u2013398. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-01244-0_34"},{"key":"52_CR8","unstructured":"Benzm\u00fcller, C.: Simple type theory as framework for combining logics. Contest paper presented at the World Congress and School on Universal Logic III (UNILOG\u20192010), Lisbon, Portugal (2010). http:\/\/arxiv.org\/abs\/1004.5500"},{"key":"52_CR9","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.E., Kohlhase M.: Higher order semantics and extensionality. J. Symb. Logic 69, 1027\u20131088 (2004)","journal-title":"J. Symb. Logic"},{"key":"52_CR10","volume-title":"Festschrift in Honor of Peter B Andrews on His 70th Birthday, Studies in Logic, Mathematical Logic and Foundations.","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller C., Paulson L.C.: Exploring properties of normal multimodal logics in simple type theory with LEO-II. In: Benzm\u00fcller, C., Brown, C.E., Siekmann, J., Statman, R. (eds) Festschrift in Honor of Peter B Andrews on His 70th Birthday, Studies in Logic, Mathematical Logic and Foundations., College Publications, London (2008)"},{"issue":"6","key":"52_CR11","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.C.: Multimodal and intuitionistic logics in simple type theory. Logic J. IGPL 18(6), 881\u2013892 (2010)","journal-title":"Logic J. IGPL"},{"key":"52_CR12","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Theiss, F., Paulson, L.C., Fietzke, A.: LEO-II\u2014a cooperative automatic theorem prover for higher-order logic. In: Armondo, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12\u201315. Proceedings, LNCS, vol. 5195. Springer, Berlin, pp 162\u2013170 (2008)","DOI":"10.1007\/978-3-540-71070-7_14"},{"key":"52_CR13","first-page":"131","volume-title":"First International Conference on Interactive Theorem Proving (ITP 2010), LNCS, vol. 6172.","author":"J.C. 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) First International Conference on Interactive Theorem Proving (ITP 2010), LNCS, vol. 6172., pp. 131\u2013146. Springer, Berlin (2010)"},{"issue":"2","key":"52_CR14","doi-asserted-by":"crossref","first-page":"257","DOI":"10.2307\/2271102","volume":"34","author":"R.A. Bull","year":"1969","unstructured":"Bull R.A.: On modal logic with propositional quantifiers. J. Symb. Logic 34(2), 257\u2013263 (1969)","journal-title":"J. Symb. Logic"},{"key":"52_CR15","doi-asserted-by":"crossref","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. Logic 5, 56\u201368 (1940)","journal-title":"J. Symb. Logic"},{"key":"52_CR16","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1111\/j.1755-2567.1970.tb00432.x","volume":"36","author":"K. Fine","year":"1970","unstructured":"Fine K.: Propositional quantifiers in modal logic. Theoria 36, 336\u2013346 (1970)","journal-title":"Theoria"},{"issue":"2","key":"52_CR17","doi-asserted-by":"crossref","first-page":"201","DOI":"10.2307\/2273727","volume":"44","author":"K. Fine","year":"1979","unstructured":"Fine K.: Failures of the interpolation lemma in quantified modal logic. J. Symb. Logic 44(2), 201\u2013206 (1979)","journal-title":"J. Symb. Logic"},{"issue":"2","key":"52_CR18","doi-asserted-by":"crossref","first-page":"621","DOI":"10.2178\/jsl\/1190150101","volume":"67","author":"M. Fitting","year":"2002","unstructured":"Fitting M.: Interpolation for first order S5. J. Symb. Logic 67(2), 621\u2013634 (2002)","journal-title":"J. Symb. Logic"},{"key":"52_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-010-0411-4","volume-title":"Types, Tableaus, and G\u00f6del\u2019s God","author":"M. Fitting","year":"2002","unstructured":"Fitting M.: Types, Tableaus, and G\u00f6del\u2019s God. Kluwer, Dordrecht (2002)"},{"key":"52_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-5292-1","volume-title":"First-order modal logic","author":"M. Fitting","year":"1998","unstructured":"Fitting M., Mendelsohn R.L.: First-order modal logic. Kluwer, Dordrecht (1998)"},{"key":"52_CR21","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"Henkin L.: Completeness in the theory of types. J. Symb. Logic 15, 81\u201391 (1950)","journal-title":"J. Symb. Logic"},{"key":"52_CR22","doi-asserted-by":"crossref","DOI":"10.4324\/9780203290644","volume-title":"A New Introduction to Modal Logic","author":"G. Hughes","year":"1996","unstructured":"Hughes G., Cresswell M.: A New Introduction to Modal Logic. Routledge, London (1996)"},{"issue":"4","key":"52_CR23","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/s10849-009-9087-8","volume":"18","author":"M. Kaminski","year":"2009","unstructured":"Kaminski M., Smolka G.: Terminating tableau systems for hybrid logic with difference and converse. J. Log. Lang. Inf. 18(4), 437\u2013464 (2009)","journal-title":"J. Log. Lang. Inf."},{"key":"52_CR24","first-page":"355","volume":"35","author":"D. Kaplan","year":"1970","unstructured":"Kaplan D.: S5 with quantifiable propositional variables. J. Symb. Logic 35, 355 (1970)","journal-title":"J. Symb. Logic"},{"issue":"2","key":"52_CR25","doi-asserted-by":"crossref","first-page":"529","DOI":"10.2307\/2275545","volume":"62","author":"P. Kremer","year":"1997","unstructured":"Kremer P.: On the complexity of propositional quantification in intuitionistic logic. J. Symb. Logic 62(2), 529\u2013544 (1997)","journal-title":"J. Symb. Logic"},{"issue":"1","key":"52_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"S. Kripke","year":"1959","unstructured":"Kripke S.: A completeness theorem in modal logic. J. Symb. Logic 24(1), 1\u201314 (1959)","journal-title":"J. Symb. Logic"},{"key":"52_CR27","doi-asserted-by":"crossref","unstructured":"Muskens, R.: Higher order modal logic. In: Blackburn, P., van Benthem, J.F.A.K., Wolter, F. (eds.) Handbook of Modal Logic, vol. 3 (Studies in Logic and Practical Reasoning). Elsevier, New York (2006)","DOI":"10.1016\/S1570-2464(07)80013-9"},{"issue":"1","key":"52_CR28","doi-asserted-by":"crossref","first-page":"98","DOI":"10.2178\/jsl\/1174668386","volume":"72","author":"R. Muskens","year":"2007","unstructured":"Muskens R.: Intensional models for the theory of types. J. Symb. Logic 72(1), 98\u2013118 (2007)","journal-title":"J. Symb. Logic"},{"key":"52_CR29","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283","author":"T. Nipkow","year":"2002","unstructured":"Nipkow T., Paulson L.C., Wenzel M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Berlin (2002)"},{"key":"52_CR30","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics, TPHOLs 2008, LNCS, vol. 5170","author":"K. Slind","year":"2008","unstructured":"Slind K., Norrish M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds) Theorem Proving in Higher Order Logics, TPHOLs 2008, LNCS, vol. 5170, pp. 28\u201332. Springer, Berlin (2008)"}],"container-title":["Logica Universalis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-012-0052-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11787-012-0052-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-012-0052-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,29]],"date-time":"2019-06-29T00:46:44Z","timestamp":1561769204000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11787-012-0052-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5,27]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["52"],"URL":"https:\/\/doi.org\/10.1007\/s11787-012-0052-y","relation":{},"ISSN":["1661-8297","1661-8300"],"issn-type":[{"value":"1661-8297","type":"print"},{"value":"1661-8300","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,5,27]]}}}