Naproche
Since 2020 I am involved in the development of Naproche – a proof assistant which features a LATEX-compatible controlled natural input language.
Naproche is available as a component of the proof assistant Isabelle which allows Naproche formalizations to be authored in Isabelle's Proof IDE and to be checked for mathematical correctness via the theorem provers that are bundled with Isabelle. Since these formalizations can be embedded into LATEX, they can directly be converted to PDF (or even HTML).
Semantic Philosophy Archive
In 2026 I launched the Semantic Philosophy Archive – a collection of semantically annotated philosophical texts together with a knowledge database these texts are interlinked with.
On the one hand, this project is an attempt to collect various versions of classical philosophical texts in multiple languages from the public domain in one place and enrich them with semantic annotations. On the other hand, it constitutes an experiment to investigate how methods and tools from mathematical knowledge management can be used to represent philosophical knowledge.