Biographie

Daniel Kirchner’s Forschungsarbeit entstand aus der Vorlesung Computational Metaphysics seines späteren Doktorvaters Christoph Benzmüller an der FU Berlin. Dort kam er erstmals sowohl mit automatisierten Beweisassistenten als auch mit Edward Zalta und seiner Abstract Object Theory in Kontakt. Sowohl Benzmüller als auch Zalta hatten bereits Grundsteine im Feld der Computational Metaphysics gelegt, also in der Anwendung von Computerverfahren auf philosophische Fragestellungen und Theorien in der Metaphysik. In diesem faszinierenden, interdisziplinären Feld siedelte Daniel dann zunächst seine Masterarbeit und später seine Doktorarbeit in Mathematik an, in der er die Logik von Zalta’s Abstract Object Theory mit Hilfe eines Shallow Semantic Embeddings im automatisierten Beweisassistenten Isabelle/HOL einbettet. Hierdurch wurden erstmals die existierenden Automatisierungsverfahren für klassische Logik höherer Stufe auf ein komplexes nicht-klassisches Logiksystem der Philosophie übertragen, was in Zusammenarbeit mit Zalta und Kollegen am Metaphysics Research Lab in Stanford zu einer erheblichen Weiterentwicklung der adressierten philosophischen Theorie führte, die als Fundamentaltheorie der Metaphysik und Grundlagentheorie für Philosophie und Mathematik dienen möchte.

Neben seiner leitenden Position in der Entwicklung der Programmiersprache Solidity für die Ethereum Foundation, setzt Daniel diese Forschungsarbeit nun am Lehrstuhl für KI-Systementwicklung der Universität Bamberg fort.

___

English:

Daniel Kirchner's research emerged from the Computational Metaphysics lecture of his future doctoral supervisor Christoph Benzmüller at the FU Berlin. It was there that he first came into contact with both automated proof assistants and Edward Zalta and his Abstract Object Theory. Both Benzmüller and Zalta had already laid foundations in the field of computational metaphysics, i.e. in the application of computer methods to philosophical questions and theories in metaphysics. It was in this fascinating, interdisciplinary field that Daniel first wrote his master's thesis and later his doctoral thesis in mathematics, in which he embedded the logic of Zalta's Abstract Object Theory in the automated proof assistant Isabelle/HOL using Shallow Semantic Embedding. This was the first time that existing automation procedures for higher-level classical logic were applied to a complex non-classical logic system of philosophy, which, in collaboration with Zalta and colleagues at the Metaphysics Research Lab at Stanford, led to a significant further development of the addressed philosophical theory, which aims to serve as a foundational theory of metaphysics and basic theory for philosophy and mathematics.

In addition to his leading position in the development of the Solidity programming language for the Ethereum Foundation, Daniel is now continuing this research work at the Chair of AI System Development at the University of Bamberg.

Fragestellungen im Themenfeld Künstliche Intelligenz

Daniel Kirchner beschäftigt sich in seiner Forschungsarbeit mit der Anwendung von automatisierten Beweisverfahren auf philosophische Theorien durch die Einbettung komplexer Logiken der formalen Metaphysik in klassische Logik.

___

English:

Daniel Kirchner's research focuses on the application of automated proof methods to philosophical theories by embedding complex logics of formal metaphysics in classical logic.