{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,3]],"date-time":"2024-06-03T16:33:56Z","timestamp":1717432436214},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2011,6,1]],"date-time":"2011-06-01T00:00:00Z","timestamp":1306886400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2011,6]]},"DOI":"10.1007\/s10472-011-9249-7","type":"journal-article","created":{"date-parts":[[2011,7,8]],"date-time":"2011-07-08T14:49:48Z","timestamp":1310136588000},"page":"103-128","source":"Crossref","is-referenced-by-count":9,"title":["Combining and automating classical and non-classical logics in classical higher-order logics"],"prefix":"10.1007","volume":"62","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,7,9]]},"reference":[{"key":"9249_CR1","doi-asserted-by":"crossref","first-page":"395","DOI":"10.2307\/2272982","volume":"37","author":"PB Andrews","year":"1972","unstructured":"Andrews, P.B.: General models and extensionality. J. Symb. Log. 37, 395\u2013397 (1972)","journal-title":"J. Symb. Log."},{"key":"9249_CR2","doi-asserted-by":"crossref","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. Symb. Log. 37, 385\u2013394 (1972)","journal-title":"J. Symb. Log."},{"issue":"2","key":"9249_CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"PB Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem proving via general matings. J. ACM 28(2), 193\u2013214 (1981)","journal-title":"J. ACM"},{"key":"9249_CR4","doi-asserted-by":"crossref","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Kluwer Academic Publishers (2002)","DOI":"10.1007\/978-94-015-9934-4"},{"issue":"3","key":"9249_CR5","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":"9249_CR6","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","volume":"4","author":"PB Andrews","year":"2006","unstructured":"Andrews, P.B., Brown, C.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Log. 4(4), 367\u2013395 (2006)","journal-title":"J. Appl. Log."},{"key":"9249_CR7","doi-asserted-by":"crossref","unstructured":"Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. In: Giesl, J., H\u00e4hnle, R. (eds.) Proceedings of Automated Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, 16\u201319 Jul 2010. Lecture Notes in Artificial Intelligence, vol. 6173, pp. 76\u201390. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_7"},{"key":"9249_CR8","unstructured":"Baldoni, M.: Normal multimodal logics: automatic deduction and logic programming extension. PhD thesis, Universita degli studi di Torino (1998)"},{"key":"9249_CR9","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C.: Extensional higher-order paramodulation and RUE-resolution. In: In Proc. of CADE-16. LNAI, number 1632, pp. 399\u2013413. Springer (1999)","DOI":"10.1007\/3-540-48660-7_39"},{"key":"9249_CR10","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, Proceedings of the 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, 18\u201320 May 2009. IFIP, vol. 297, pp. 387\u2013398. Springer (2009)","DOI":"10.1007\/978-3-642-01244-0_34"},{"key":"9249_CR11","series-title":"Lecture Notes in Artificial Intelligence","first-page":"33","volume-title":"Computational Logic in Multi-Agent Systems, Proceedings of the 11th International Workshop, CLIMA XI, Lisbon, Portugal, 16\u201317 Aug 2010","author":"C Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C.: Combining logics in simple type theory. In: Dix, J., Leite, J., Governatori, G., Jamroga, W. (eds.) Computational Logic in Multi-Agent Systems, Proceedings of the 11th International Workshop, CLIMA XI, Lisbon, Portugal, 16\u201317 Aug 2010. Lecture Notes in Artificial Intelligence, vol. 6245, pp. 33\u201348. Springer, Lisbon, Portugal (2010)"},{"key":"9249_CR12","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C.: Verifying the modal logic cube is an easy task (for higher-order automated reasoners). In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis\u2014Festschrift for Christoph Walther on the Occasion of His 60th Birthday. LNCS, vol. 6463, pp. 117\u2013128. Springer (2010)","DOI":"10.1007\/978-3-642-17172-7_7"},{"key":"9249_CR13","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. Log. 69, 1027\u20131088 (2004)","journal-title":"J. Symb. Log."},{"key":"9249_CR14","series-title":"Lecture Notes in Artificial Intelligence, number 1421","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/BFb0054256","volume-title":"Automated Deduction\u2014CADE-15, Proceedings of the 15th International Conference on Automated Deduction, Lindau, Germany, 5\u201310 Jul 1998","author":"C Benzm\u00fcller","year":"1998","unstructured":"Benzm\u00fcller, C., Kohlhase, M.: LEO\u2014a higher-order theorem prover. In: Kirchner, C., Kirchner, H. (eds.) Automated Deduction\u2014CADE-15, Proceedings of the 15th International Conference on Automated Deduction, Lindau, Germany, 5\u201310 Jul 1998. Lecture Notes in Artificial Intelligence, number 1421, pp. 139\u2013143. Springer, Lindau, Germany (1998)"},{"key":"9249_CR15","unstructured":"Benzm\u00fcller, C., Paulson, L.C.: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, chapter Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. Studies in Logic, Mathematical Logic and Foundations. College Publications (2008)"},{"key":"9249_CR16","unstructured":"Benzm\u00fcller, C., Paulson, L.C.: Quantified Multimodal Logics in Simple Type Theory. SEKI Report SR\u20132009\u201302 (ISSN 1437\u20134447). SEKI Publications, DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str. 5, D\u201328359 Bremen, Germany http:\/\/arxiv.org\/abs\/0905.2435 (2009)"},{"key":"9249_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.C.: Multimodal and intuitionistic logics in simple type theory. Log J IGPL 18, 881\u2013892 (2010)","journal-title":"Log J IGPL"},{"key":"9249_CR18","unstructured":"Benzm\u00fcller, C., Pease, A.: Progress in automating higher-order ontology reasoning. In: Konev, B., Schmidt, R., Schulz, S. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), Edinburgh, UK. CEUR Workshop Proceedings (2010)"},{"key":"9249_CR19","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.) Proceedings of the ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10), Lisbon, Portugal, 16\u201317 Aug 2010"},{"key":"9249_CR20","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Rabe, F., Sutcliffe, G.: THF0\u2014the core TPTP language for classical higher-order logic. In: Baumgartner, P., Armando, A., Gilles, D. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, number 5195, pp. 491\u2013506. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_41"},{"key":"9249_CR21","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Theiss, F., Paulson, L., Fietzke, A.: LEO-II\u2014a cooperative automatic theorem prover for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.), Automated Reasoning, Proceedings of the 4th International Joint Conference, IJCAR 2008, Sydney, Australia, 12\u201315 Aug 2008. Lecture Notes in Artificial Intelligence, vol. 5195, pp. 162\u2013170. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_14"},{"key":"9249_CR22","volume-title":"Handbook of Modal Logic, vol. 3 (Studies in Logic and Practical Reasoning)","author":"P Blackburn","year":"2006","unstructured":"Blackburn, P., van Benthem, J.F.A.K., Wolter, F.: Handbook of Modal Logic, vol. 3 (Studies in Logic and Practical Reasoning). Elsevier Science Inc., New York, NY, USA (2006)"},{"key":"9249_CR23","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1004991115882","volume":"59","author":"P Blackburn","year":"1995","unstructured":"Blackburn, P., de\u00a0Rijke, M.: Why combine logics? Stud. Log. 59, 5\u201327 (1995)","journal-title":"Stud. Log."},{"key":"9249_CR24","doi-asserted-by":"crossref","unstructured":"Blackburn, P., Marx, M.: Tableaux for quantified hybrid logic. In: Egly, U., Ferm\u00fcller, C.G. (eds.) Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2002, Copenhagen, Denmark, 30 Jul\u20131 Aug 2002. Lecture Notes in Computer Science, vol. 2381, pp. 38\u201352. Springer (2002)","DOI":"10.1007\/3-540-45616-3_4"},{"issue":"2","key":"9249_CR25","doi-asserted-by":"crossref","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. J. Logic Lang. Inf. 14(2), 173\u2013198, (2005)","journal-title":"J. Logic Lang. Inf."},{"key":"9249_CR26","unstructured":"Brown, C.: Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church\u2019s Type Theory. Studies in Logic: Logic and Cognitive Systems, number\u00a010. College Publications (2007)"},{"key":"9249_CR27","unstructured":"Carnielli, W., Coniglio, M.E.: Combining logics. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Winter 2008 edition (2008)"},{"key":"9249_CR28","series-title":"Applied Logic Series","volume-title":"Analysis and synthesis of logics: how to cut and paste reasoning systems; electronic version","author":"WA Carnielli","year":"2008","unstructured":"Carnielli, W.A., Coniglio, M., Gabbay, D.M., Gouveia, P., Sernadas, C.: Analysis and synthesis of logics: how to cut and paste reasoning systems; electronic version. Applied Logic Series. Springer, Dordrecht (2008)"},{"key":"9249_CR29","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. Log. 5, 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"issue":"2","key":"9249_CR30","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. Log. 67(2), 621\u2013634 (2002)","journal-title":"J. Symb. Log."},{"issue":"4","key":"9249_CR31","doi-asserted-by":"crossref","first-page":"1057","DOI":"10.2307\/2275807","volume":"61","author":"DM Gabbay","year":"1996","unstructured":"Gabbay, D.M.: Fibred semantics and the weaving of logics, part 1: Modal and intuitionistic logics. J. Symb. Log. 61(4), 1057\u20131120 (1996)","journal-title":"J. Symb. Log."},{"key":"9249_CR32","unstructured":"Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional modal logics: theory and applications. Studies in Logic, vol. 148. Elsevier Science (2003)"},{"key":"9249_CR33","doi-asserted-by":"crossref","unstructured":"Garg, D., Abadi, M.: A modal deconstruction of access control logics. In: Amadio, R. (ed.) Proceedings of the 11th International Conference on the Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science, number 4962, pp. 216\u2013230 (2008)","DOI":"10.1007\/978-3-540-78499-9_16"},{"key":"9249_CR34","unstructured":"Garson, J.: Modal logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Winter 2009 edition (2009)"},{"key":"9249_CR35","unstructured":"G\u00f6del, K.: Eine interpretation des intuitionistischen aussagenkalk\u00fcls. Ergebnisse eines Mathematischen Kolloquiums, 8, 39\u201340 (1933) Also published in G\u00f6del, K.: Collected Works, Volume I, pp. 296\u2013302. Oxford University Press (1986)"},{"key":"9249_CR36","unstructured":"Goldblatt, R.: Logics of time and computation. Center for the Study of Language and Information - Lecture Notes, number\u00a07. Leland Stanford Junior University (1992)"},{"key":"9249_CR37","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. Log. 15, 81\u201391 (1950)","journal-title":"J. Symb. Log."},{"key":"9249_CR38","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di\u00a0Vito, B., Munoz, C. (eds.) Proceedings of the 1st International Workshop on Design and Application of Strategies\/Tactics in Higher Order Logics. NASA Technical Reports, number NASA\/CP-2003-212448, pp. 56\u201368 (2003)"},{"issue":"4","key":"9249_CR39","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. Logic Lang. Inf. 18(4), 437\u2013464 (2009)","journal-title":"J. Logic Lang. Inf."},{"key":"9249_CR40","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2268135","volume":"13","author":"JCC McKinsey","year":"1948","unstructured":"McKinsey, J.C.C., Tarski, A.: Some theorems about the sentential calculi of lewis and heyting. J. Symb. Log. 13, 1\u201315 (1948)","journal-title":"J. Symb. Log."},{"issue":"4","key":"9249_CR41","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"D Miller","year":"1987","unstructured":"Miller, D.: A Compact Representation of Proofs. Stud. Log. 46(4), 347\u2013370 (1987)","journal-title":"Stud. Log."},{"key":"9249_CR42","doi-asserted-by":"crossref","unstructured":"Nguyen, L.A.: MProlog: an extension of prolog for modal logic programming. In: Demoen, B., Lifschitz, V. (eds.) Logic Programming, Proceedings of the 20th International Conference, ICLP 2004, Saint-Malo, France, 6\u201310 Sept 2004. Lecture Notes in Computer Science, vol. 3132, pp. 469\u2013470. Springer (2004)","DOI":"10.1007\/978-3-540-27775-0_42"},{"key":"9249_CR43","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/j.tcs.2006.03.026","volume":"360","author":"LA Nguyen","year":"2006","unstructured":"Nguyen, L.A.: Multimodal logic programming. Theor. Comp. Sci. 360, 247\u2013288 (2006)","journal-title":"Theor. Comp. Sci."},{"issue":"2","key":"9249_CR44","doi-asserted-by":"crossref","first-page":"167","DOI":"10.3166\/jancl.19.167-181","volume":"19","author":"LA Nguyen","year":"2009","unstructured":"Nguyen, L.A.: Modal logic programming revisited. J. Appl. Non-Class. Log. 19(2), 167\u2013181 (2009)","journal-title":"J. Appl. Non-Class. Log."},{"key":"9249_CR45","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, number 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9249_CR46","doi-asserted-by":"crossref","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001","volume-title":"Past, Present and Future","author":"AN Prior","year":"1967","unstructured":"Prior, A.N.: Past, Present and Future. Clarendon Press, Oxford (1967)"},{"key":"9249_CR47","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":"2\/3","key":"9249_CR48","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E\u2014a Brainiac theorem prover. Journal of AI Commun. 15(2\/3), 111\u2013126 (2002)","journal-title":"Journal of AI Commun"},{"issue":"1","key":"9249_CR49","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF02115610","volume":"2","author":"K Segerberg","year":"1973","unstructured":"Segerberg, K.: Two-dimensional modal logic. J. Philos. Logic 2(1), 77\u201396 (1973)","journal-title":"J. Philos. Logic"},{"key":"9249_CR50","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. Lecture Notes in Computer Science, number 4649, pp. 7\u201323. Springer (2007)"},{"key":"9249_CR51","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP World\u2014infrastructure for automated reasoning. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning\u201416th International Conference, LPAR-16, Dakar, Senegal, 25 Apr\u20131 May 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol. 6355, pp. 1\u201312. Springer (2010)","DOI":"10.1007\/978-3-642-17511-4_1"},{"issue":"1","key":"9249_CR52","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 3(1), 1\u201327 (2010)","journal-title":"Journal of Formalized Reasoning"},{"key":"9249_CR53","doi-asserted-by":"crossref","unstructured":"Thomason, R.H.: Combinations of tense and modality. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic. Extensions of Classical Logic, vol. 2, pp. 135\u2013165. D. Reidel (1984)","DOI":"10.1007\/978-94-009-6259-0_3"},{"key":"9249_CR54","unstructured":"Venema, Y.: In: Goble, L. (ed.) The Blackwell Guide to Philosophical Logic, chapter Venema, Yde, Temporal Logic. Blackwell Publishing http:\/\/www.blackwellreference.com\/public\/book?id=g9780631206934_9780631206934 (2001)."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-011-9249-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-011-9249-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-011-9249-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,27]],"date-time":"2021-11-27T19:42:56Z","timestamp":1638042176000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-011-9249-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6]]},"references-count":54,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["9249"],"URL":"https:\/\/doi.org\/10.1007\/s10472-011-9249-7","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,6]]}}}