{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:59:21Z","timestamp":1743069561657,"version":"3.40.3"},"publisher-location":"Cham","reference-count":73,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319217673"},{"type":"electronic","value":"9783319217680"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","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":[[2015]]},"DOI":"10.1007\/978-3-319-21768-0_2","type":"book-chapter","created":{"date-parts":[[2015,7,10]],"date-time":"2015-07-10T12:35:20Z","timestamp":1436531720000},"page":"32-74","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Higher-Order Modal Logics: Automation and Applications"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[]},{"given":"Bruno","family":"Woltzenlogel Paleo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,11]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Web semantics: Science, services and agents on the world wide web, special issue on reasoning with context in the semantic web, vol. 12\u201313, pp. 1\u2013160 (2012)","DOI":"10.1016\/j.websem.2011.12.004"},{"key":"2_CR2","volume-title":"Kurt G\u00f6del, Collected Works","author":"RM Adams","year":"1995","unstructured":"Adams, R.M.: Introductory Note to *1970. In: Feferman, S., et al. (eds.) Kurt G\u00f6del, Collected Works, vol. III. Oxford University Press, New York (1995)"},{"issue":"3","key":"2_CR3","first-page":"55","volume":"17","author":"V Akman","year":"1996","unstructured":"Akman, V., Surav, M.: Steps toward formalizing context. AI Mag. 17(3), 55\u201372 (1996)","journal-title":"AI Mag."},{"issue":"2","key":"2_CR4","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","volume":"52","author":"J Alama","year":"2014","unstructured":"Alama, J., Heskes, T., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning 52(2), 191\u2013213 (2014)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR5","series-title":"Lecture Notes in Logic","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-662-21963-8_10","volume-title":"G\u00f6del \u201996: Logical foundations of mathematics, computer science and physics","author":"AC Anderson","year":"1996","unstructured":"Anderson, A.C., Gettings, M.: G\u00f6del\u2019s ontological proof revisited. In: H\u00e1jek, P. (ed.) G\u00f6del \u201996: Logical foundations of mathematics, computer science and physics. Lecture Notes in Logic, vol. 6, pp. 167\u2013172. Springer, Berlin (1996)"},{"issue":"2","key":"2_CR6","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. Symb. Logic 37(2), 395\u2013397 (1972)","journal-title":"J. Symb. Logic"},{"key":"2_CR7","unstructured":"Andrews, P.B.: Church\u2019s type theory. In: Zalta, E.N. (ed.), The Stanford Encyclopedia of Philosophy. Spring 2014 edition, 2014"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Andrews, P.B., Miller, D.A.: Eve Longini Cohen, and Frank Pfenning. Automating higher-order logic. In: Bledsoe, W.W., Loveland, D.W., et al., Automated Theorem Proving: After 25 Years, vol. 29 of Contemporary Mathematics series, pp. 169\u2013192. American Mathematical Society (1984)","DOI":"10.1090\/conm\/029\/09"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61208-4_1","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"PB Andrews","year":"1996","unstructured":"Andrews, P.B., Bishop, M.: On sets, types, fixed points, and checkerboards. In: Miglioli, P., Moscato, U., Mundici, D., Ornaghi, D. (eds.) Theorem Proving with Analytic Tableaux and Related Methods. LNCS, vol. 1071, pp. 1\u201315. Springer, Heidelberg (1996)"},{"key":"2_CR10","unstructured":"Marcos, J.: Modality and paraconsistency. The Logica Yearbook, pp. 213\u2013222 (2005)"},{"volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","year":"2003","key":"2_CR11","unstructured":"Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, New York (2003)"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Theiss, F., Paulson, L., Fietzke, A.: LEO-II - a cooperative automatic theorem prover for higher-order logic. In: Proceedings of IJCAR 2008, number 5195 in LNAI, pp. 162\u2013170. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-71070-7_14"},{"key":"2_CR13","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: Formalization, Mechanization and Automation of G\u00f6del\u2019s Proof of God\u2019s Existence. arXiv: 1308.4526 (2013)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-17172-7_7","volume-title":"Verification, Induction, Termination Analysis","author":"C Benzm\u00fcller","year":"2010","unstructured":"Benzm\u00fcller, C.: Verifying the modal logic cube is an easy task (for higher-order automated reasoners). In: Siegler, S., Wasser, N. (eds.) Walther Festschrift. LNCS, vol. 6463, pp. 117\u2013128. Springer, Heidelberg (2010)"},{"key":"2_CR15","series-title":"Studies in Logic, Grammar, and Rhetoric","first-page":"299","volume-title":"From Insight to Proof - Festschrift in Honour of Andrzej Trybulec","author":"C Benzm\u00fcller","year":"2007","unstructured":"Benzm\u00fcller, C., Brown, C.: The curious inference of Boolos in MIZAR and OMEGA. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof - Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar, and Rhetoric, vol. 10(23), pp. 299\u2013388. The University of Bialystok, Polen (2007)"},{"issue":"4","key":"2_CR16","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. Symb. Logic 69(4), 1027\u20131088 (2004)","journal-title":"J. Symb. Logic"},{"key":"2_CR17","unstructured":"Benzm\u00fcller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: Raedt, L.D., Bessiere, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P. (eds.), ECAI 2012, Frontiers in Artificial Intelligence and Applications, vol. 242, pp. 163\u2013168. IOS Press, Montpellier (2012)"},{"key":"2_CR18","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: G\u00f6del\u2019s God in Isabelle\/HOL. Arch. Formal Proofs, 2013 (2013)"},{"key":"2_CR19","unstructured":"Benzm\u00fcller, C., Woltzenlogel Paleo, B.: Automating G\u00f6del\u2019s ontological proof of God\u2019s existence with higher-order automated theorem provers. In: Schaub, T., Friedrich, G., O\u2019Sullivan, B., (eds.), ECAI 2014, Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93\u201398, IOS Press (2014)"},{"key":"2_CR20","unstructured":"Benzm\u00fcller, C., Paulson, L.: Exploring properties of normal multimodal logics in simple type theory with LEO-II. In: Benzm\u00fcller, C., Brown, C., Siekmann, J., Statman, R. (eds.), Reasoning in Simple Type Theory \u2013 Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic, Mathematical Logic and Foundations, pp. 386\u2013406, College Publications (2008)"},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","volume":"7","author":"C Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logic Univers. (Spec. Issue Multimodal Logics) 7(1), 7\u201320 (2013)","journal-title":"Logic Univers. (Spec. Issue Multimodal Logics)"},{"key":"2_CR22","first-page":"104","volume":"12\u201313","author":"C Benzm\u00fcller","year":"2012","unstructured":"Benzm\u00fcller, C., Pease, A.: Higher-order aspects and context in SUMO. J. Web Seman. (Spec. Issue Reasoning with context in the Semant. Web) 12\u201313, 104\u2013117 (2012)","journal-title":"J. Web Seman. (Spec. Issue Reasoning with context in the Semant. Web)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-45221-5_9","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Christoph Benzm\u00fcller","year":"2013","unstructured":"Benzm\u00fcller, Christoph, Raths, Thomas: HOL based first-order modal logic provers. In: McMillan, Ken, Middeldorp, Aart, Voronkov, Andrei (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 127\u2013136. Springer, Heidelberg (2013)"},{"key":"2_CR24","unstructured":"Benzm\u00fcller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-H\u00e1jek ontological controversy. In: Silvestre, R.S., B\u00e9ziau, J.-Y. (eds.), Handbook of the 1st World Congress on Logic and Religion, Joao Pessoa, Brasil (2015)"},{"key":"2_CR25","volume-title":"Handbook of Paraconsistency","author":"JY Beziau","year":"2007","unstructured":"Beziau, J.Y., Carnielli, W., Gabbay, D.: Handbook of Paraconsistency. College Publications, London (2007)"},{"key":"2_CR26","volume-title":"Handbook of Modal Logic, Volume 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, Volume 3 (Studies in Logic and Practical Reasoning). Elsevier Science Inc., New York (2006)"},{"issue":"1","key":"2_CR27","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. Reasoning 51(1), 109\u2013128 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR28","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":"Jasmin Christian Blanchette","year":"2010","unstructured":"Blanchette, Jasmin Christian, Nipkow, Tobias: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, Matt, Paulson, Lawrence C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131\u2013146. Springer, Heidelberg (2010)"},{"key":"2_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00250612","volume":"16","author":"G Boolos","year":"1987","unstructured":"Boolos, G.: A curious inference. J. Philos. Logic 16, 1\u201312 (1987)","journal-title":"J. Philos. Logic"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","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 automated higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning. LNCS, vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012)"},{"issue":"3","key":"2_CR31","first-page":"263","volume":"23","author":"S Bucav","year":"1995","unstructured":"Bucav, S., Buvac, V., Mason, I.A.: Metamathematics of contexts. Fundamenta Informaticae 23(3), 263\u2013301 (1995)","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"2_CR32","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","volume":"49","author":"A Chargu\u00e9raud","year":"2012","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. J. Autom. Reasoning 49(3), 363\u2013408 (2012)","journal-title":"J. Autom. Reasoning"},{"key":"2_CR33","unstructured":"Corazzon, R.: Contemporary bibliography on ontological arguments. http:\/\/www.ontology.co\/biblio\/ontological-proof-contemporary-biblio.htm"},{"issue":"4","key":"2_CR34","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1305\/ndjfl\/1093888132","volume":"18","author":"NCA da Costa","year":"1977","unstructured":"da Costa, N.C.A., Alves, E.H.: Semantical analysis of the calculi cn. Notre Dame J. Formal Logic 18(4), 621\u2013630 (1977)","journal-title":"Notre Dame J. Formal Logic"},{"key":"2_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-94-017-0460-1_1","volume":"6","author":"JM Dunn","year":"2002","unstructured":"Dunn, J.M., Restall, G.: Relevance logic. Handbook of Philosophical Logic 6, 1\u2013136 (2002)","journal-title":"Handbook of Philosophical Logic"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Fitting, M.: Types, Tableaux and G\u00f6del\u2019s God, Kluwer (2002)","DOI":"10.1007\/978-94-010-0411-4"},{"key":"2_CR37","series-title":"Synthese Library","doi-asserted-by":"publisher","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. Synthese Library. Kluwer, Netherlands (1998)"},{"key":"2_CR38","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labelled Deductive Systems","author":"DM Gabbay","year":"1996","unstructured":"Gabbay, D.M.: Labelled Deductive Systems. Clarendon Press, Oxford (1996)"},{"key":"2_CR39","volume-title":"Intensional and Higher-Order Modal Logic","author":"D Gallin","year":"1975","unstructured":"Gallin, D.: Intensional and Higher-Order Modal Logic. North Holland, New York (1975)"},{"key":"2_CR40","first-page":"345","volume":"16","author":"F Giunchiglia","year":"1993","unstructured":"Giunchiglia, F.: Contextual reasoning. Epistemologia (Special Issue on Languages and Machines) 16, 345\u2013364 (1993)","journal-title":"Epistemologia (Special Issue on Languages and Machines)"},{"issue":"1","key":"2_CR41","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/0004-3702(94)90037-X","volume":"65","author":"F Giunchiglia","year":"1994","unstructured":"Giunchiglia, F., Serafini, L.: Multilanguage hierarchical logics or: How we can do without modal logics. Artif. Intell. 65(1), 29\u201370 (1994)","journal-title":"Artif. Intell."},{"key":"2_CR42","first-page":"65","volume-title":"Ontological Proof","author":"K G\u00f6del","year":"1970","unstructured":"G\u00f6del, K.: Collected Works, Unpublished Essays and Letters. Ontological Proof, pp. 65\u201385. Oxford University Press, Oxford (1970)"},{"key":"2_CR43","unstructured":"G\u00f6del, K.: Appx.A: Notes in Kurt G\u00f6del\u2019s Hand. In: [70], pp. 144\u2013145 (2004)"},{"key":"2_CR44","unstructured":"Guha, R.V.: Context: A Formalization and Some Applications. Ph.D. thesis, Stanford University (1991)"},{"issue":"2","key":"2_CR45","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. Symb. Logic 15(2), 81\u201391 (1950)","journal-title":"J. Symb. Logic"},{"issue":"5","key":"2_CR46","first-page":"55","volume":"1","author":"S Ja\u015bkowski","year":"1948","unstructured":"Ja\u015bkowski, S.: Rachunek zda\u0144 dla system\u00f3w dedukcyjnych sprzecznych. Stud. Soc. Scientiarun Torunesis 1(5), 55\u201377 (1948)","journal-title":"Stud. Soc. Scientiarun Torunesis"},{"key":"2_CR47","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/BF02134311","volume":"24","author":"S Ja\u015bkowski","year":"1969","unstructured":"Ja\u015bkowski, S.: Propositional calculus for contradictory deductive systems. Stud. Logica. 24, 143\u2013157 (1969)","journal-title":"Stud. Logica."},{"issue":"1","key":"2_CR48","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Hol(y)hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","journal-title":"Math. Comput. Sci."},{"key":"2_CR49","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.jsc.2014.09.032","volume":"69","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69, 109\u2013128 (2015)","journal-title":"J. Symb. Comput."},{"key":"2_CR50","unstructured":"Lindblad, F.: agsyHOL website. https:\/\/github.com\/frelindb\/agsyHOL"},{"issue":"12","key":"2_CR51","doi-asserted-by":"publisher","first-page":"1030","DOI":"10.1145\/33447.33448","volume":"30","author":"J McCarthy","year":"1987","unstructured":"McCarthy, J.: Generality in artificial intelligence. Commun. ACM 30(12), 1030\u20131035 (1987)","journal-title":"Commun. ACM"},{"key":"2_CR52","unstructured":"McCarthy, J.: Notes on formalizing context. In: Proceedings of IJCAI 1993, pp. 555\u2013562 (1993)"},{"key":"2_CR53","first-page":"621","volume-title":"Handbook of Modal Logic","author":"R Muskens","year":"2006","unstructured":"Muskens, R.: Higher order modal logic. In: Blackburn, P., et al. (eds.) Handbook of Modal Logic, pp. 621\u2013653. Elsevier, Dordrecht (2006)"},{"key":"2_CR54","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. 2283. Springer, Berlin (2002)"},{"key":"2_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/978-3-319-08587-6_20","volume-title":"Automated Reasoning","author":"J Otten","year":"2014","unstructured":"Otten, J.: Mleancop: A connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning. LNCS, vol. 8562, pp. 269\u2013276. Springer, Switzerland (2014)"},{"key":"2_CR56","unstructured":"Woltzenlogel Paleo, B., Benzm\u00fcller, C.: Formal theology repository. (https:\/\/github.com\/FormalTheology\/GoedelGod)"},{"key":"2_CR57","unstructured":"Paulin-Mohring, C.: Introduction to the calculus of inductive constructions. In: Delahaye, D., Woltzenlogel Paleo, B. (eds.), All about Proofs, Proofs for All, Mathematical Logic and Foundations. College Publications, London (2015)"},{"key":"2_CR58","volume-title":"Ontology: A Practical Guide","author":"A Pease","year":"2011","unstructured":"Pease, A.: Ontology: A Practical Guide. Articulate Software Press, Angwin (2011)"},{"key":"2_CR59","unstructured":"Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.), Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories (ESARLT), CEUR Workshop Proceedings, vol. 257, CEUR-WS.org (2007)"},{"key":"2_CR60","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1111\/j.1755-2567.2001.tb00204.x","volume":"67","author":"G Priest","year":"2001","unstructured":"Priest, G.: Paraconsistent belief revision. Theoria 67, 214\u2013228 (2001)","journal-title":"Theoria"},{"key":"2_CR61","doi-asserted-by":"crossref","unstructured":"Priest, G., Sylvan, R.: Simplified semantics for basic relevant logics. J. Philos. Logic (1992)","DOI":"10.1007\/BF00248640"},{"key":"2_CR62","unstructured":"Ramachandran, D., Reagan, P., Goolsbey, K.: First-orderized ResearchCyc: Expressivity and efficiency in a common-sense ontology. In: Shvaiko P. (ed.), Papers from the AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications, Pittsburgh, Pennsylvania, USA, 2005. Technical report WS-05-01 published by The AAAI Press, Menlo Park, California, July 2005"},{"key":"2_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-642-31365-3_35","volume-title":"Automated Reasoning","author":"Thomas Raths","year":"2012","unstructured":"Raths, Thomas, Otten, Jens: The QMLTP problem library for first-order modal logics. In: Gramlich, Bernhard, Miller, Dale, Sattler, Uli (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 454\u2013461. Springer, Heidelberg (2012)"},{"key":"2_CR64","unstructured":"Restall, G., Slaney, J.: Realistic belief revision. In: Proceedings of the Second World Conference in the Fundamentals of Artificial Intelligence, pp. 367\u2013378 (1995)"},{"key":"2_CR65","doi-asserted-by":"crossref","unstructured":"Scott, D.: Appx.B: Notes in Dana Scott\u2019s Hand. In: [70], pp. 145\u2013146 (2004)","DOI":"10.1016\/j.tvjl.2005.04.016"},{"key":"2_CR66","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.artint.2003.11.001","volume":"155","author":"L Serafini","year":"2004","unstructured":"Serafini, L., Bouquet, P.: Comparing formal theories of context in AI. Artif. Intell. 155, 41\u201367 (2004)","journal-title":"Artif. Intell."},{"key":"2_CR67","unstructured":"Siders, A., Woltzenlogel Paleo, B.: A variant of G\u00f6del\u2019s ontological proof in a natural deduction calculus. ( github.com\/FormalTheology\/GoedelGod\/blob\/master\/Papers\/InProgress\/NaturalDeduction\/GodProof-ND.pdf?raw=true)"},{"key":"2_CR68","unstructured":"Sobel, J.H.: G\u00f6del\u2019s ontological proof. In On Being and Saying. Essays for Richard Cartwright, pp. 241\u2013261, MIT Press (1987)"},{"key":"2_CR69","volume-title":"Logic and Theism: Arguments for and Against Beliefs in God","author":"JH Sobel","year":"2004","unstructured":"Sobel, J.H.: Logic and Theism: Arguments for and Against Beliefs in God. Cambridge University Press, Cambridge (2004)"},{"issue":"4","key":"2_CR70","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 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"2_CR71","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. Formalized Reasoning 3(1), 1\u201327 (2010)","journal-title":"J. Formalized Reasoning"},{"key":"2_CR72","doi-asserted-by":"crossref","first-page":"28","DOI":"10.26686\/ajl.v1i0.1761","volume":"1","author":"K Tanaka","year":"2003","unstructured":"Tanaka, K.: Three schools of paraconsistency. The Australas. J. Logic 1, 28\u201342 (2003)","journal-title":"The Australas. J. Logic"},{"key":"2_CR73","unstructured":"Wenzel, M.: Hoare logic in isabelle. http:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/HOL-Isar_Examples\/Hoare.html"}],"container-title":["Lecture Notes in Computer Science","Reasoning Web. Web Logic Rules"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21768-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,9]],"date-time":"2024-06-09T22:50:26Z","timestamp":1717973426000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21768-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319217673","9783319217680"],"references-count":73,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21768-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"11 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}