This project aims to formalize several ontological arguments and the "Simulation Argument" by Nick Bostrom in Isabelle/HOL using a shallow semantic embedding. It is part of an ongoing effort to see if and how automatic theorem provers can help solve problems in mathematics and philosophy.

Student

David Streit

Mentors

  • Bruno Woltzenlogel Paleo
  • Christoph Benzm├╝ller
close

2017