Automated Reasoning; Universal Reasoning; Semantic Embedding; Higher Order Logic
Résumé :
[en] The quest for a most general framework supporting universal reasoning is very prominently represented in the works of Leibniz. He envisioned a scientia generalis founded on a characteristica universalis, that is, a most universal formal language in which all knowledge about the world and the sciences can be encoded. A quick study of the survey literature on logical formalisms suggests that quite the opposite to Leibniz’ dream has become reality. Instead of a characteristica universalis, we are today facing a very rich and heterogenous zoo of different logical systems, and instead of converging towards a single superior logic, this logic zoo is further expanding, eventually even at accelerated pace. As a consequence, the unified vision of Leibniz seems farther away than ever before. However, there are also some promising initiatives to counteract these diverging developments. Attempts at unifying approaches to logic include categorial logic algebraic logic and coalgebraic logic.
Disciplines :
Arts & sciences humaines: Multidisciplinaire, généralités & autres Philosophie & éthique Sciences informatiques Mathématiques
Auteur, co-auteur :
BENZMÜLLER, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Co-auteurs externes :
no
Langue du document :
Anglais
Titre :
Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract)
Date de publication/diffusion :
11 novembre 2017
Nom de la manifestation :
Brazilian Symposium on Formal Methods
Date de la manifestation :
from 27-11-2017 to 1-12-2017
Sur invitation :
Oui
Manifestation à portée :
International
Titre de l'ouvrage principal :
Formal Methods: Foundations and Applications - 20th Brazilian Symposium SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings
Bentert, M., Benzmüller, C., Streit, D., Woltzenlogel Paleo, B.: Analysis of an ontological proof proposed by Leibniz. In: Tandy, C. (ed.) Death and Anti-Death. Four Decades after Michael Polanyi, Three Centuries after G.W. Leibniz, vol. 14. Ria University Press (2016)
Benzmüller, C.: Automating access control logics in simple type theory with LEO-II. In: Gritzalis, D., Lopez, J. (eds.) SEC 2009. IAICT, vol. 297, pp. 387–398. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-01244-0 34
Benzmüller, C.: Combining and automating classical and non-classical logics in classical higher-order logic. Ann. Math. Artif. Intell. (Special Issue Computational logics in Multi-agent Systems (CLIMA XI)) 62(1–2), 103–128 (2011)
Benzmüller, C.: Automating quantified conditional logics in HOL. In: Rossi, F. (ed.) IJCAI 2013, pp. 746–753. AAAI Press (2013)
Benzmüller, C.: Cut-elimination for quantified conditional logic. J. Philos. Logic 46(3), 333–353 (2017)
Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Gabbay, D.M., Siekmann, J.H., Woods, J. (eds.) Handbook of the History of Logic. Computational Logic, vol. 9, pp. 215–254. North Holland, Elsevier (2014)
Benzmüller, C., Paulson, L.: Multimodal and intuitionistic logics in simple type theory. Logic J. IGPL 18(6), 881–892 (2010)
Benzmüller, C., Paulson, L.: Quantified multimodal logics in simple type theory. Logica Univ. (Special Issue on Multimodal Logics) 7(1), 7–20 (2013)
Benzmüller, C., Paulson, L.C., Sultana, N., Theiß, F.: The higher-order prover LEO-II. J. Autom. Reasoning 55(4), 389–404 (2015)
Benzmüller, C., Scott, D.S.: Axiomatizing category theory in free logic (2016). arXiv, http://arxiv.org/abs/1609.01493
Benzmüller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-Hájek controversy. Logica Univ. 11(1), 139–151 (2017)
Benzmüller, C., Woltzenlogel Paleo, B.: Gödel’s God in Isabelle/HOL. Archive of Formal Proofs (2013). (Formally verified)
Benzmüller, C., Woltzenlogel Paleo, B.: Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. In: Schaub, T., Friedrich, G., O’Sullivan, B. (eds.) ECAI 2014. Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93–98. IOS Press (2014)
Benzmüller, C., Woltzenlogel Paleo, B.: Interacting with modal logics in the coq proof assistant. In: Beklemishev, L.D., Musatov, D.V. (eds.) CSR 2015. LNCS, vol. 9139, pp. 398–411. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20297-6 25
Benzmüller, C., Woltzenlogel Paleo, B.: The inconsistency in Gödel’s ontological argument: a success story for AI in metaphysics. In: Kambhampati, S. (ed.) IJCAI 2016. vol. 1–3, pp. 936–942. AAAI Press (2016)
Benzmüller, C., Paleo, B.W.: The ontological modal collapse as a collapse of the square of opposition. In: Béziau, J.-Y., Basti, G. (eds.) The Square of Opposition: A Cornerstone of Thought. SUL, pp. 307–313. Springer, Cham (2017). https://doi. org/10.1007/978-3-319-45062-9 18
Benzmüller, C., Woltzenlogel Paleo, B.: Experiments in Computational Metaphysics: Gödel’s proof of God’s existence. Savijnanam: scientific exploration for a spiritual paradigm. J. Bhaktivedanta Inst. 9, 43–57 (2017)
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)
Boolos, G.: The Logic of Provability. Cambridge University Press, Cambridge (1993)
Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5, 56–68 (1940)
Fitting, M.: Types, Tableaus, and Gödel’s God. Kluwer, Amsterdam (2002)
Freyd, P.J., Scedrov, A.: Categories. North Holland, Allegories (1990)
Fuenmayor, D., Benzmüller, C.: Automating emendations of the ontological argument in intensional higher-order modal logic. In: Kern-Isberner, G., Fürnkranz, J., Thimm, M. (eds.) KI 2017. Lecture Notes in Computer Science, vol. 10505, pp. 114–127. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67190-1 9
Gödel, K.: Appx. A: Notes in Kurt Gödel’s Hand. In: Sobel [33], pp. 144–145 (1970)
Kirchner, D.: Representation and partial automation of the principia logico-metaphysica in Isabelle/HOL. Archive of Formal Proofs (2017). formally verified with Isabelle/HOL
Lachnitt, H.: Systematic verification of the intuitionistic modal logic cube in isabelle/hol. Bachelor Thesis at the Freie Universität Berlin, Institut für Informatik (2017)
Oppenheimer, P.E., Zalta, E.N.: Relations versus functions at the foundations of logic: type-theoretic considerations. J. Log. Comput. 21(2), 351–374 (2011)
Scott, D.: Appx. B: Notes in Dana Scott’s Hand. In: Sobel [33], pp. 145–146 (1972)
Scott, D.: Existence and description in formal logic. In: Schoenman, R. (ed.) Bertrand Russell: Philosopher of the Century, pp. 181–200. George Allen & Unwin, London (1967). (Reprinted with additions. In: Philosophical Application of Free Logic, edited by K. Lambert. Oxford Universitry Press, 1991, pp. 28–48)
Sobel, J.: Logic and Theism. Cambridge U. Press, Cambridge (2004)
Steen, A., Benzmüller, C.: Sweet SIXTEEN: automation via embedding into classical higher-order logic. Logic Logical Philos. 25, 535–554 (2016)
Steen, A., Wisniewski, M., Benzmüller, C.: Tutorial on reasoning in expressive non-classical logics with Isabelle/HOL. In: Benzüller, C., Rojas, R., Sutcliffe, G. (eds.) GCAI 2016. EPiC Series in Computing, vol. 41, pp. 1–10. EasyChair (2016)
Wisniewski, M., Steen, A., Benzmüller, C.: Einsatz von Theorembeweisern in der Lehre. In: Schwill, A., Lucke, U. (eds.) Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik. Commentarii informaticae didacticae (CID), Universitätsverlag Potsdam, Potsdam, Germany (2016)
