Johannes C. Schuster

I recently completed my Master’s degree in Applied Computer Science at the University of Bamberg, with a research focus on artificial intelligence. My thesis was supervised by Prof. Dr. Christoph Benzmüller (chair for AI Systems Engineering), at whose chair I continue to work and plan to pursue a Ph.D.

Throughout my studies, I have focussed heavily on the theoretical foundations of machine learning and automated theorem proving. My core expertise lies in higher-order logics, the mathematics for machine learning, natural language processing, functional programming and neuro-symbolic AI.

Much of my current work is infrastructure for automated reasoning on the BEAM (Elixir/Erlang): tptp, a parser, linter and printer for the TPTP language; AtpClient, uniform access to external provers; and Shot, the concurrent higher-order tableau prover I developed in my thesis. Together with Geoff Sutcliffe (University of Miami), I am revising the SZS ontologies, the standard in which automated reasoning systems report their result status; I have formalised the success ontology in Isabelle/HOL, from which the hierarchy is derived and against which the published grammar is checked.

My planned doctoral project, Certified Parallel Tableaux for Higher-Order Logics with Language Model Instantiations, builds on Shot. It develops a free-variable tableau calculus for classical higher-order logic with destructive substitution and OR-parallel search over instantiation candidates, and aims to prove it sound and complete with respect to Henkin semantics with choice. A language model is to propose instantiations inside the search, the calculus checks every proposal, and every answer is to come with a certificate that a small independent verifier checks against an explicit axiomatisation of higher-order logic. A transfer of the calculus to dependently typed higher-order logic is planned as an extension.