Studies in Computational Metaphysics

• Applicant: Professor Dr.-Ing. Christoph Benzmüller
• Subject Area: Theoretical Computer Science ; Image and Language Processing, Computer Graphics and Visualisation, Human Computer Interaction, Ubiquitous and Wearable Computing ; Theoretical Philosophy
• Term: from 2012 to 2017
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 215348714

• Final Report Year: 2017

Final Report Abstract

The core contributions of this Heisenberg Project include (i) a theoretical framework towards universal logic reasoning (which utilises classical higher-order logic as a universal meta-logic), (ii) the “implementation” of the approach in higher-order interactive and automated theorem provers, (iii) the exemplary application of the approach in selected fields of philosophy, mathematics and computer science, (iv) the education of a new generation of students to master the approach, and (v) the dissemination and communication of the results to different scientific communities (philosophy, artificial intelligence, computer science and mathematics) and to the wider public.

Publications

• Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers. Frontiers in Artificial Intelligence and Applications, Vol. 263: ECAI 2014, pp. 93 - 98.
  Christoph Benzmüller, Bruno Woltzenlogel-Paleo.
  (See online at https://dx.doi.org/10.3233/978-1-61499-419-0-93)
• Automation of Higher-Order Logic. In: Handbook of the History of Logic, Vol. 9: Computational Logic. Ed. by Dov M. Gabbay, Jörg H. Siekmann, John Woods. North Holland, Elsevier, 2014, pp. 215–254.
  Christoph Benzmüller, Dale Miller
  (See online at https://doi.org/10.1016/B978-0-444-51624-4.50005-8)
• The Higher-Order Prover LEO-II. Journal of Automated Reasoning, Vol. 55. 2015, Issue 4, pp. 389–404.
  Christoph Benzmüller, Lawrence C. Paulson, Nik Sultana, Frank Thei.
  (See online at https://doi.org/10.1007/s10817-015-9348-y)
• Cut-Elimination for Quantified Conditional Logic. Journal of Philosophical Logic, Vol. 46. 2017, Issue 3, pp. 333–353.
  Christoph Benzmüller
  (See online at https://doi.org/10.1007/s10992-016-9403-0)
• The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In IJCAI 2016 (Subbarao Kambhampati, ed.), AAAI Press, Vol. 1-3. 2016, pp. 936-942.
  Christoph Benzmüller
  
• Computer-Assisted Analysis of the Anderson-H´ajek Controversy. Logica Universalis, Vol. 11. 2017, Issue 1, pp. 139–151.
  Christoph Benzmüller, Leon Weber, Bruno Woltzenlogel-Paleo
  (See online at https://doi.org/10.1007/s11787-017-0160-9)
• Universal (Meta-)Logical Reasoning: Recent Successes 2018. (Preprint)
  Christoph Benzmüller
  (See online at https://doi.org/10.13140/RG.2.2.11039.61609/2)
• Universal (Meta-)Logical Reasoning: Recent Successes. In: Science of Computer Programming, Vol. 172. 2019, pp. 48-62.
  Christoph Benzmüller)
  (See online at https://doi.org/10.1016/j.scico.2018.10.008)