Logo der Freien Universität BerlinFreie Universität Berlin

Fachbereich Mathematik und Informatik


Service-Navigation

  • Startseite
  • Personen
  • Kontakt
  • Imprint
  • Datenschutz
Hinweise zur Datenübertragung bei der Google™ Suche
Fachbereich Mathematik und Informatik/Informatik/

Dahlem Center for Machine Learning and Robotics

Menü
  • Members

    loading...

  • Open Positions

    loading...

  • Publications

    loading...

  • Teaching

    loading...

  • Theses

    loading...

  • Projekte

    loading...

  • News

    loading...

  • Videos

    loading...

  • FAQs

    loading...

Mikronavigation

  • Startseite
  • Informatik
  • Arbeitsgruppen
  • Dahlem Center for Machine Learning and Robotics
  • Publications
  • Types, Tableaus and Gödel's God in Isabelle/HOL

Types, Tableaus and Gödel's God in Isabelle/HOL

Christoph Benzmüller, David Fuenmayor – 2017

A computer-formalisation of the essential parts of Fitting's textbook "Types, Tableaus and Gödel's God" in Isabelle/HOL is presented. In particular, Fitting's (and Anderson's) variant of the ontological argument is verified and confirmed. This variant avoids the modal collapse, which has been criticised as an undesirable side-effect of Kurt Gödel's (and Dana Scott's) versions of the ontological argument. Fitting's work is employing an intensional higher-order modal logic, which we shallowly embed here in classical higher-order logic. We then utilize the embedded logic for the formalisation of Fitting's argument. (See also the earlier AFP entry ``Gödel's God in Isabelle/HOL''

Titel
Types, Tableaus and Gödel's God in Isabelle/HOL
Verfasser
Christoph Benzmüller, David Fuenmayor
Datum
2017-05-01
Kennung
ISSN: 2150-914x
Quelle/n
  • pdf-Datei
Erschienen in
Archive of Formal Proofs, 2017
BibTeX Code
Bibtex entry URL: bibtexbrowser.local.php?key=J35&bib=chris.bib
be-digital Pressekonferenz am 07.12.15Mexico Oktober 2015MiG Mexico 2015Finalisten German Open 2014Simulator-Erfinder: Professor Raul Rojas (l.) und David Dormagen von der AG Intelligente Systeme und RobotikMadeInGermany in MexicoThe Tony Sale Award winners 2014: Robert B Garner (L) and  Raul Rojas (R), Nov. 2014Able und BakerCarolo-Cup-Team2014Formalisierung und Automatisierung von Gödels GottesbeweisAutoNOMOS-Team 2011Besuch Senatorin Yzer am 22.03.13Die autonomen Fahrzeuge der AG Intelligente Systeme und RobotikArchaeocopterMulticopterEntwicklung einer RoboterbienePreisverleihung bei der Dubai Challenge

Dates

spinner

News

spinner

Service-Navigation

  • Startseite
  • Personen
  • Kontakt
  • Imprint
  • Datenschutz

Diese Seite

  • Drucken
  • RSS-Feed abonnieren