Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract)

Benzmüller, Christoph

doi:10.1007/978-3-319-70848-5_2

Download

Paper published in a book (Scientific congresses, symposiums and conference proceedings)

Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract)

Benzmüller, Christoph

2017 • In Benzmüller, Christoph (Ed.) Formal Methods: Foundations and Applications - 20th Brazilian Symposium SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings

Permalink
https://hdl.handle.net/10993/33609

DOI
10.1007/978-3-319-70848-5_2

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

C66.pdf

Author preprint (72.31 kB)

Download

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

Automated Reasoning; Universal Reasoning; Semantic Embedding; Higher Order Logic

Abstract :

[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 & humanities: Multidisciplinary, general & others
Philosophy & ethics
Computer science
Mathematics

Author, co-author :

Benzmüller, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)

External co-authors :

Language :

English

Title :

Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract)

Publication date :

11 November 2017

Event name :

Brazilian Symposium on Formal Methods

Event date :

from 27-11-2017 to 1-12-2017

By request :

Yes

Audience :

International

Main work title :

Formal Methods: Foundations and Applications - 20th Brazilian Symposium SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings

Author, co-author :

Benzmüller, Christoph

Publisher :

Springer

ISBN/EAN :

978-3-319-70847-8

Collection name :

Lecture Notes in Computer Science

Pages :

7-11

Focus Area :

Computational Sciences

Additional URL :

http://christoph-benzmueller.de/papers/C66.pdf

Commentary :

7--11 10623

Available on ORBilu :

since 12 December 2017

Statistics

Number of views

132 (3 by Unilu)

Number of downloads

147 (0 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

Bibliography

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.: Automating Free Logic in Isabelle/HOL. In: Greuel, G.-M., Koch, T., Paule, P., Sommese, A. (eds.) ICMS 2016. LNCS, vol. 9725, pp. 43–50. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42432-3 6
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)
Lambert, K.: Free Logic. Selected Essays. Cambridge University Press, Cambridge (2012)
Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9
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)
Zalta, E.N.: Principia logico-metaphysica (2016). draft version, preprint https://mally.stanford.edu/principia.pdf