{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:56:48Z","timestamp":1725562608006},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642149764"},{"type":"electronic","value":"9783642149771"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14977-1_6","type":"book-chapter","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T06:23:30Z","timestamp":1281507810000},"page":"33-48","source":"Crossref","is-referenced-by-count":0,"title":["Combining Logics in Simple Type Theory"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"publisher","first-page":"395","DOI":"10.2307\/2272982","volume":"37","author":"P.B. Andrews","year":"1972","unstructured":"Andrews, P.B.: General models and extensionality. Journal of Symbolic Logic\u00a037, 395\u2013397 (1972)","journal-title":"Journal of Symbolic Logic"},{"key":"6_CR2","doi-asserted-by":"publisher","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. Journal of Symbolic Logic\u00a037, 385\u2013394 (1972)","journal-title":"Journal of Symbolic Logic"},{"key":"6_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 Academic Publishers, Dordrecht (2002)","edition":"2"},{"issue":"4","key":"6_CR4","doi-asserted-by":"publisher","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. Journal of Applied Logic\u00a04(4), 367\u2013395 (2006)","journal-title":"Journal of Applied Logic"},{"key":"6_CR5","series-title":"LNAI","volume-title":"IJCAR 2010 - 5th International Joint Conference on Automated Reasoning","author":"J. Backes","year":"2010","unstructured":"Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. In: Giesl, J., Haehnle, R. (eds.) IJCAR 2010 - 5th International Joint Conference on Automated Reasoning, Edinburgh, UK. LNCS (LNAI). Springer, Heidelberg (2010)"},{"key":"6_CR6","unstructured":"Baldoni, M.: Normal Multimodal Logics: Automatic Deduction and Logic Programming Extension. PhD thesis, Universita degli studi di Torino (1998)"},{"key":"6_CR7","series-title":"IFIP","first-page":"387","volume-title":"Proceedings of 24th IFIP TC 11 International Information Security Conference, SEC 2009, Emerging Challenges for Security, Privacy and Trust, Pafos, Cyprus","author":"C. Benzm\u00fcller","year":"2009","unstructured":"Benzm\u00fcller, C.: Automating access control logic in simple type theory with LEO-II. In: Gritzalis, D., L\u00f3pez, J. (eds.) Proceedings of 24th IFIP TC 11 International Information Security Conference, SEC 2009, Emerging Challenges for Security, Privacy and Trust, Pafos, Cyprus, May 18-20. IFIP, vol.\u00a0297, pp. 387\u2013398. Springer, Heidelberg (2009)"},{"key":"6_CR8","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. Journal of Symbolic Logic\u00a069, 1027\u20131088 (2004)","journal-title":"Journal of Symbolic Logic"},{"key":"6_CR9","unstructured":"Benzm\u00fcller, C., Paulson, L.: Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. In: Festschrift in Honor of Peter B. Andrews on His 70th Birthday. Studies in Logic, Mathematical Logic and Foundations. College Publications (2008)"},{"key":"6_CR10","unstructured":"Benzm\u00fcller, C., Paulson, L.C.: Quantified Multimodal Logics in Simple Type Theory. SEKI Report SR\u20132009\u201302, SEKI Publications, DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str. 5, D\u201328359 Bremen, Germany (2009), ISSN 1437-4447, http:\/\/arxiv.org\/abs\/0905.2435"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory. The Logic Journal of the IGPL (2010)","DOI":"10.1093\/jigpal\/jzp080"},{"key":"6_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II \u2014 A Cooperative Automatic Theorem Prover for Higher-Order Logic. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 162\u2013170. Springer, Heidelberg (2008)"},{"key":"6_CR13","unstructured":"Benzm\u00fcller, C., Pease, A.: Progress in automating higher-order ontology reasoning. In: Konev, B., Schmidt, R., Schulz, S. (eds.) Workshop on Practical Aspects of Automated Reasoning (PAAR 2010), Edinburgh, UK, July 14. CEUR Workshop Proceedings (2010)"},{"key":"6_CR14","unstructured":"Benzm\u00fcller, C., Pease, A.: Reasoning with embedded formulas and modalities in SUMO. In: Bundy, A., Lehmann, J., Qi, G., Varzinczak, I.J. (eds.) The ECAI 2010 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE 2010), Lisbon, Portugal, August 16-17 (2010)"},{"key":"6_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-71070-7_41","volume-title":"Automated Reasoning","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Rabe, F., Sutcliffe, G.: THF0 \u2014 The Core TPTP Language for Classical Higher-Order Logic. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 491\u2013506. Springer, Heidelberg (2008)"},{"key":"6_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-45616-3_4","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"P. Blackburn","year":"2002","unstructured":"Blackburn, P., Marx, M.: Tableaux for quantified hybrid logic. In: Egly, U., Ferm\u00fcller, C.G. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 38\u201352. Springer, Heidelberg (2002)"},{"issue":"2","key":"6_CR17","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10849-005-3927-y","volume":"14","author":"T. Bra\u00fcner","year":"2005","unstructured":"Bra\u00fcner, T.: Natural deduction for first-order hybrid logic. Journal of Logic, Language and Information\u00a014(2), 173\u2013198 (2005)","journal-title":"Journal of Logic, Language and Information"},{"key":"6_CR18","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. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"6_CR19","doi-asserted-by":"publisher","first-page":"621","DOI":"10.2178\/jsl\/1190150101","volume":"67","author":"M. Fitting","year":"2002","unstructured":"Fitting, M.: Interpolation for first order S5. Journal of Symbolic Logic\u00a067(2), 621\u2013634 (2002)","journal-title":"Journal of Symbolic Logic"},{"key":"6_CR20","series-title":"Studies in Logic","volume-title":"Many-dimensional modal logics: theory and applications","author":"D. Gabbay","year":"2003","unstructured":"Gabbay, D., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional modal logics: theory and applications. Studies in Logic, vol.\u00a0148. Elsevier Science, Amsterdam (2003)"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-78499-9_16","volume-title":"Foundations of Software Science and Computational Structures","author":"D. Garg","year":"2008","unstructured":"Garg, D., Abadi, M.: A Modal Deconstruction of Access Control Logics. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 216\u2013230. Springer, Heidelberg (2008)"},{"key":"6_CR22","unstructured":"Garson, J.: Modal logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (Winter 2009)"},{"key":"#cr-split#-6_CR23.1","unstructured":"G??del, K.: Eine interpretation des intuitionistischen aussagenkalk??ls. Ergebnisse eines Mathematischen Kolloquiums??8, 39???40 (1933);"},{"key":"#cr-split#-6_CR23.2","unstructured":"Also published in G??del [24], pp. 296???302"},{"key":"6_CR24","volume-title":"Collected Works","author":"K. G\u00f6del","year":"1986","unstructured":"G\u00f6del, K.: Collected Works, vol.\u00a0I. Oxford University Press, Oxford (1986)"},{"key":"6_CR25","unstructured":"Goldblatt, R.: Logics of Time and Computation. Center for the Study of Language and Information - Lecture Notes, vol.\u00a07. Leland Stanford Junior University (1992)"},{"key":"6_CR26","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. Journal of Symbolic Logic\u00a015, 81\u201391 (1950)","journal-title":"Journal of Symbolic Logic"},{"issue":"4","key":"6_CR27","doi-asserted-by":"publisher","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. Journal of Logic, Language and Information\u00a018(4), 437\u2013464 (2009)","journal-title":"Journal of Logic, Language and Information"},{"key":"6_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2268135","volume":"13","author":"J.C.C. McKinsey","year":"1948","unstructured":"McKinsey, J.C.C., Tarski, A.: Some theorems about the sentential calculi of lewis and heyting. Journal of Symbolic Logic\u00a013, 1\u201315 (1948)","journal-title":"Journal of Symbolic Logic"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"6_CR30","unstructured":"Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection. In: Proceedings 3rd International Conference on Knowledge Representation and Reasoning, pp. 165\u2013176 (1992)"},{"issue":"1","key":"6_CR31","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF02115610","volume":"2","author":"K. Segerberg","year":"1973","unstructured":"Segerberg, K.: Two-dimensional modal logic. Journal of Philosophical Logic\u00a02(1), 77\u201396 (1973)","journal-title":"Journal of Philosophical Logic"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-540-74510-5_4","volume-title":"Computer Science \u2013 Theory and Applications","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol.\u00a04649, pp. 6\u201322. Springer, Heidelberg (2007)"},{"issue":"4","key":"6_CR33","doi-asserted-by":"publisher","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. Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"6_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. Journal of Formalized Reasoning\u00a03(1), 1\u201327 (2010)","journal-title":"Journal of Formalized Reasoning"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-02959-2_8","volume-title":"Automated Deduction \u2013 CADE-22","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G., Benzm\u00fcller, C., Brown, C., Theiss, F.: Progress in the development of automated theorem proving for higher-order logic. In: Schmidt, R.A. (ed.) Automated Deduction \u2013 CADE-22. LNCS, vol.\u00a05663, pp. 116\u2013130. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Computational Logic in Multi-Agent Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14977-1_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:59:54Z","timestamp":1606168794000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14977-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642149764","9783642149771"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14977-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}