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.
  
• 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
  
• 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.
  
• Cut-Elimination for Quantified Conditional Logic. Journal of Philosophical Logic, Vol. 46. 2017, Issue 3, pp. 333–353.
  Christoph Benzmüller
  
• 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
  
• Universal (Meta-)Logical Reasoning: Recent Successes 2018. (Preprint)
  Christoph Benzmüller
  
• Universal (Meta-)Logical Reasoning: Recent Successes. In: Science of Computer Programming, Vol. 172. 2019, pp. 48-62.
  Christoph Benzmüller)